Stream: Coq users

Topic: ✔ Typeclass instance for mutually inductive types


view this post on Zulip Tan Yee Jian (Dec 07 2022 at 01:25):

Oh my, that was insanely helpful, especially the tip on destructing the "larger" hypothesis destruct (H n0) which gave me a lot more to work with, and the organization of code by a intermediate lemma, Coq can match the induction principle much better that way. Very happy, thanks once again!

view this post on Zulip Notification Bot (Dec 07 2022 at 01:25):

Tan Yee Jian has marked this topic as resolved.


Last updated: Jan 27 2023 at 01:03 UTC