Stream: Ltac2

Topic: Debugging, Std.set, patterns


view this post on Zulip Patrick Nicodemus (Oct 19 2022 at 20:52):

Hello, I am quite new to Ltac2 so I would appreciate any help in figuring out what I am doing wrong here.

EDIT: deleted stuff not relevant to the core problem

view this post on Zulip Patrick Nicodemus (Oct 19 2022 at 20:52):

Ltac2 hideme2 constrval :=
  let h := Fresh.in_goal @tempvar in
  Std.set
    Init.false
    (fun () => (Init.Some h, constrval))
    { Std.on_hyps := Init.None ;
                     Std.on_concl := Std.AllOccurrences }.

Goal forall (a b c d : nat), a + b + c + d = 5.
Proof.
  intros a b c d.
  (* let h := Fresh.in_goal @tempvar in *)
  (* Std.set Init.false (fun () => (Init.Some h, open_constr:(_ + _))) *)
  (*                { Std.on_hyps := Init.None ; Std.on_concl := Std.AllOccurrences }. *)
  hideme2 ( open_constr:(_ + _)).

view this post on Zulip Patrick Nicodemus (Oct 19 2022 at 20:55):

In the script above, the script "hideme2" is supposed to take in constr and change it out

view this post on Zulip Patrick Nicodemus (Oct 19 2022 at 20:56):

My problem is that Std.set does not successfully patternmatch. I expect the very last line to add tempvar := a + b + c + d : nat to the context. However, it instead adds tempvar := ?n + ?m : nat. This is confusing to me. I also was under the impression that the flag Init.false as the first argument to Std.set should cause the command to fail if it cannot find a match without evars, so even if it could not match I do not understand why it succeeds.

view this post on Zulip Patrick Nicodemus (Oct 19 2022 at 20:57):

The code that is commented out has the expected behavior, it adds H := a + b + c + d : nat to the context.

view this post on Zulip Gaëtan Gilbert (Oct 19 2022 at 21:42):

you need to thunk the constr argument
using false makes it fail if there are new evars, and they are new iff they are produced by the thunk argument

view this post on Zulip Patrick Nicodemus (Oct 19 2022 at 22:27):

Thank you! Can you tell me where this kind of thing is documented?

view this post on Zulip Patrick Nicodemus (Oct 20 2022 at 00:08):

Also, another documentation question, what is the difference between Some [] and None in the on_hyps field of Std.clause? Where can I read about this?


Last updated: Jul 24 2024 at 13:02 UTC