Jacob Salzberg (Dec 17 2023 at 18:03): Jacob Salzberg (Dec 17 2023 at 18:03):it gives me
Error: Syntax error: 'end' expected after [branches] (in [term_match]).
:(
Gaëtan Gilbert (Dec 17 2023 at 18:04):?y isn't valid for a gallina match pattern
Gaëtan Gilbert (Dec 17 2023 at 18:04):also it seems you want
Ltac destruct_let :=
match goal with
| [H : (match ?y with | _ => _ end) |- _] => destruct y
end.
oh wait, yes indeed, haha sorry
Notification Bot (Dec 17 2023 at 18:04):Jacob Salzberg has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC