Fail to generate equation lemmas?

Stream: new members

[Andrew Tindall]

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)