Stream: Coq users

Topic: ✔ Match let in Ltac


view this post on Zulip Jacob Salzberg (Dec 17 2023 at 18:03):

it gives me
Error: Syntax error: 'end' expected after [branches] (in [term_match]).
:(

view this post on Zulip Gaëtan Gilbert (Dec 17 2023 at 18:04):

?y isn't valid for a gallina match pattern

view this post on Zulip 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.

view this post on Zulip Jacob Salzberg (Dec 17 2023 at 18:04):

oh wait, yes indeed, haha sorry

view this post on Zulip Notification Bot (Dec 17 2023 at 18:04):

Jacob Salzberg has marked this topic as resolved.


Last updated: Jun 22 2024 at 16:02 UTC