Hello, I am quite new to Ltac2 so I would appreciate any help in figuring out what I am doing wrong here.
Ltac2 Type pattern_type := [ SetPattern (Init.constr) | SetInPattern (Init.pattern) ].
Ltac2 rec hideme pattern_list tac :=
match pattern_list with
| [] => tac
| head :: tail =>
match head with
| SetPattern p =>
let h := Fresh.in_goal @tempvar in
Std.set
Init.false
(fun () => (Init.Some h, p))
{ Std.on_hyps := Init.None ;
Std.on_concl := Std.AllOccurrences }
| SetInPattern p => tac
end
end.
Goal forall (a b c d : nat), a + b + c + d = 5.
Proof.
intros a b c d.
(* Std.set Init.false (fun () => (Init.Some @H, open_constr:(_ + _))) *)
(* { Std.on_hyps := Init.None ; Std.on_concl := Std.AllOccurrences }. *)
hideme (SetPattern open_constr:(_ + _) :: []) ().
In the script above, the script "hideme" is supposed to take in a list of (open) constr's and patterns, and it should iterate through the list and run either "set h := p", where p is the open_constr, or do something else if it's a pattern
My problem is that in the body of this loop, 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.
The code that is commented out has the expected behavior, it adds H := a + b + c + d : nat
to the context.
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
Thank you! Can you tell me where this kind of thing is documented?
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: Jan 31 2023 at 11:01 UTC