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: Oct 15 2021 at 20:02 UTC