Stream: Coq users

Topic: ✔ Ltac hypothesis label as argument


view this post on Zulip João Mendes (Jun 26 2023 at 21:02):

Thanks! It worked when I did this:

Ltac test label P :=
  lazymatch type of label with
  | ?H =>
    let H0 := fresh "H0" in
    assert (H0 : H \/ P);
    [ left; auto | ]
  end.

view this post on Zulip Notification Bot (Jun 26 2023 at 21:02):

João Mendes has marked this topic as resolved.

view this post on Zulip Gaëtan Gilbert (Jun 26 2023 at 21:27):

why use lazymatch instead of let?

view this post on Zulip João Mendes (Jul 05 2023 at 14:27):

In the example I brought here to explain the problem, it would work well with let. But, in the context of the actual problem, I do need lazymatch to use correctly part of the binded expression in the assert


Last updated: Jun 23 2024 at 03:02 UTC