Is there an OCaml function for eta reduction, i.e. to go from
fun x y z => <term> x y z to
Termops.eta_reduce_head is probably what you are looking for.
Thanks! Not sure how I missed that one. It even has an intuitive name :)
Last updated: Feb 01 2023 at 16:03 UTC