blob: 370bc70d1535acd980a5b095eb53f4956ad9ec5f (
plain)
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
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
|
Require Import Ltac2.Ltac2.
Ltac2 foo (_ : int) :=
let f (x : int) := x in
let _ := f 0 in
f 1.
Print Ltac2 foo.
Import Control.
Ltac2 exact x := refine (fun () => x).
Print Ltac2 refine.
Print Ltac2 exact.
Ltac2 foo' () := ident:(bla).
Print Ltac2 foo'.
Ltac2 bar x h := match x with
| None => constr:(fun H => ltac2:(exact (hyp ident:(H))) -> nat)
| Some x => x
end.
Print Ltac2 bar.
Ltac2 qux := Some 0.
Print Ltac2 qux.
Ltac2 Type foo := [ Foo (int) ].
Fail Ltac2 qux0 := Foo None.
Ltac2 Type 'a ref := { mutable contents : 'a }.
Fail Ltac2 qux0 := { contents := None }.
Ltac2 foo0 () := { contents := None }.
Print Ltac2 foo0.
Ltac2 qux0 x := x.(contents).
Ltac2 qux1 x := x.(contents) := x.(contents).
Ltac2 qux2 := ([1;2], true).
Print Ltac2 qux0.
Print Ltac2 qux1.
Print Ltac2 qux2.
Import Control.
Ltac2 qux3 x := constr:(nat -> ltac2:(refine (fun () => hyp x))).
Print Ltac2 qux3.
Ltac2 Type rec nat := [ O | S (nat) ].
Ltac2 message_of_nat n :=
let rec aux n :=
match n with
| O => Message.of_string "O"
| S n => Message.concat (Message.of_string "S") (aux n)
end in aux n.
Print Ltac2 message_of_nat.
Ltac2 numgoals () :=
let r := { contents := O } in
enter (fun () => r.(contents) := S (r.(contents)));
r.(contents).
Print Ltac2 numgoals.
Goal True /\ False.
Proof.
let n := numgoals () in Message.print (message_of_nat n).
refine (fun () => open_constr:((fun x => conj _ _) 0)); ().
let n := numgoals () in Message.print (message_of_nat n).
Fail (hyp ident:(x)).
Fail (enter (fun () => hyp ident:(There_is_no_spoon); ())).
enter (fun () => Message.print (Message.of_string "foo")).
enter (fun () => Message.print (Message.of_constr (goal ()))).
Fail enter (fun () => Message.print (Message.of_constr (qux3 ident:(x)))).
enter (fun () => plus (fun () => constr:(_); ()) (fun _ => ())).
plus
(fun () => enter (fun () => let x := ident:(foo) in let _ := hyp x in ())) (fun _ => Message.print (Message.of_string "failed")).
let x := { contents := 0 } in
let x := x.(contents) := x.(contents) in x.
Abort.
Ltac2 Type exn ::= [ Foo ].
Goal True.
Proof.
plus (fun () => zero Foo) (fun _ => ()).
Abort.
Ltac2 Type exn ::= [ Bar (string) ].
Goal True.
Proof.
Fail zero (Bar "lol").
Abort.
Ltac2 Notation "refine!" c(thunk(constr)) := refine c.
Goal True.
Proof.
refine! I.
Abort.
Goal True.
Proof.
let x () := plus (fun () => 0) (fun _ => 1) in
match case x with
| Val x =>
match x with
| (x, k) => Message.print (Message.of_int (k Not_found))
end
| Err x => Message.print (Message.of_string "Err")
end.
Abort.
Goal (forall n : nat, n = 0 -> False) -> True.
Proof.
refine (fun () => '(fun H => _)).
Std.case true (hyp @H, Std.ExplicitBindings [Std.NamedHyp @n, '0]).
refine (fun () => 'eq_refl).
Qed.
Goal forall x, 1 + x = x + 1.
Proof.
refine (fun () => '(fun x => _)).
Std.cbv {
Std.rBeta := true; Std.rMatch := true; Std.rFix := true; Std.rCofix := true;
Std.rZeta := true; Std.rDelta := true; Std.rConst := [];
} { Std.on_hyps := None; Std.on_concl := Std.AllOccurrences }.
Abort.
|
