Stream: Coq users

Topic: `Let` produces beta-redexes

Paolo Giarrusso (Jan 26 2021 at 14:22):

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: Apr 19 2024 at 16:01 UTC