Stream: Coq users

Topic: ✔ Correctly unfold function definition


view this post on Zulip Eduardo Freire (Aug 11 2022 at 17:26):

Ah, this helped me find what I was looking for. Apparently the Function package automatically defines bubble_equation, which is the unfolding lemma I wanted. I will definitely look into Equations though, thank you!

view this post on Zulip Notification Bot (Aug 11 2022 at 17:27):

Eduardo Freire has marked this topic as resolved.

view this post on Zulip Pierre Courtieu (Aug 12 2022 at 08:44):

You have equation and induction lemmas defined automatically (for non dependently typed functions only). But indeed Function is getting old and Equations subsumes it almost every aspects.


Last updated: Feb 06 2023 at 12:04 UTC