1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
Require Import Ltac2.Ltac2.
Fail Ltac2 my_change1 (a : constr) (b : constr) :=
change $a with $b.
Fail Ltac2 my_change2 (a:preterm) (b:constr) :=
change $preterm:a with $b.
(* This is pretty bad, maybe $x should mean $pattern:x in patterns?
Main question is if we allow preterm in pattern, is
"fun x => let y := preterm:($x) in pattern:($preterm:y)"
going to be confusing? (x must be constr, and we error at runtime??)
Instead don't allow preterms, instead expose "pattern_of_preterm : preterm -> pattern",
having runtime errors there seems more sensible than with the quotation.
*)
Ltac2 my_change3 (a:pattern) (b:constr) :=
change $pattern:a with $b.
Fail Ltac2 dummy x := preterm:($pattern:x).
Goal id True -> False.
Fail match! goal with [ |- True -> False ] => () end.
my_change3 pat:(id True) constr:(True).
match! goal with [ |- True -> False ] => () end.
Fail let a := preterm:(id True) in change $preterm:a with True.
Abort.
|
