Zulip Chat Archive

Stream: new members

Topic: Fail to generate equation lemmas?

view this post on Zulip Andrew Tindall (Jan 12 2019 at 00:23):

I have a function that I defined recursively by cases on an inductive type. If i set_option eqn_compiler.lemmas false it compiles, but simp cannot use it ( simp debug ). if I set_option eqn_compiler.lemmas true it does not compile ( eqn_compiler debug ). I can't tell from either of these where the error is - is there some other trace option I can turn on, maybe?

(@Mario Carneiro , I am also thinking this is a problem that might just disappear when Jesse OKs your pull request defining inductive dfins instead of fins)

Last updated: May 08 2021 at 02:46 UTC