Since tactics like eauto
don't unfold definitions, we'd often like to pre-unfold them in lemma statements — Let
would be convenient but it produces beta-redexes. Is that semantics useful? Is there a good fix, other than reimplementing Let
eval unfold foo in foo ...
?
Notation Unfold x tm := (* XXX can only unfold one definition *)
ltac:(let H := eval unfold x in tm in exact H) (only parsing).
Definition statement_template args := ...
Lemma statement_1 : Unfold statement_template (statement_template args1). ...
Lemma statement_2 : Unfold statement_template (statement_template args2). ...
Last updated: Oct 13 2024 at 01:02 UTC