Stream: Coq devs & plugin devs

Topic: Eta reduction


view this post on Zulip Janno (Jul 30 2020 at 08:51):

Is there an OCaml function for eta reduction, i.e. to go from fun x y z => <term> x y z to <term>?

view this post on Zulip Hugo Herbelin (Jul 31 2020 at 04:40):

@Janno Termops.eta_reduce_head is probably what you are looking for.

view this post on Zulip Janno (Jul 31 2020 at 10:27):

Thanks! Not sure how I missed that one. It even has an intuitive name :)


Last updated: Oct 15 2021 at 20:02 UTC