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
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
|
Require Import Ltac2.Ltac2.
Ltac2 Type exn ::= [ Got (Std.intro_pattern option) ].
(* we can't return a value from a ltac1 notation so we get it out using Control.zero *)
Tactic Notation "foo" simple_intropattern(x) :=
let f := ltac2:(y |- Control.zero (Got (Ltac1.to_intro_pattern y))) in
f x.
Ltac2 Notation "ipat" x(intropattern) := x.
Goal nat. (* we need an open goal because ltac1 auto focuses *)
Ltac2 Eval match Control.case (fun () => ltac1:(foo y%nat)) with
| Err (Got (Some (Std.IntroAction
(Std.IntroApplyOn
c
(Std.IntroNaming (Std.IntroIdentifier id)))))) =>
Control.assert_true (Ident.equal id @y);
match! c () with
| nat => ()
| _ => Control.throw Assertion_failure
end
| Val _ | Err _ => Control.throw Assertion_failure
end.
Ltac2 Eval match Ltac1.to_intro_pattern (Ltac1.of_intro_pattern (ipat ?w)) with
| Some (Std.IntroNaming (Std.IntroFresh id)) => Control.assert_true (Ident.equal id @w)
| _ => Control.throw Assertion_failure
end.
Ltac2 Eval
ltac1:(
let n := numgoals in
let t := ltac2:(n |-
match Ltac1.to_int n with
| Some 1 => ()
| _ => Control.throw Assertion_failure
end)
in
t n).
Fail Ltac2 Eval
ltac1:(
let n := numgoals in
let t := ltac2:(n |-
match Ltac1.to_int n with
| None => ()
| _ => Control.throw Assertion_failure
end)
in
t n).
Ltac2 Eval
ltac1:(n |- do n assert False; [| | |]) (Ltac1.of_int 2).
Abort.
|
