Patrick Nicodemus (Oct 19 2022 at 20:52): 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
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:(_ + _)).
In the script above, the script "hideme2" is supposed to take in constr and change it out
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.
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.
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
Patrick Nicodemus (Oct 19 2022 at 22:27):Thank you! Can you tell me where this kind of thing is documented?
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: Oct 08 2024 at 16:02 UTC