blob: 9108871e28a99f6398b4b89799df081741e68e5a (
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
|
Require Import Ltac2.Ltac2 Ltac2.Notations.
Ltac2 mutable foo () := constructor.
Goal True.
Proof.
foo ().
Qed.
Ltac2 Set foo := fun _ => fail.
Goal True.
Proof.
Fail foo ().
constructor.
Qed.
(** Bindings are dynamic *)
Ltac2 Type rec nat := [O | S (nat)].
Ltac2 rec nat_eq n m :=
match n with
| O => match m with | O => true | S _ => false end
| S n => match m with | O => false | S m => nat_eq n m end
end.
Ltac2 assert_eq n m :=
match nat_eq n m with
| true => ()
| false => Control.throw Assertion_failure end.
Ltac2 mutable x := O.
Ltac2 y := x.
Ltac2 Eval (assert_eq y O).
Ltac2 Set x := (S O).
Ltac2 Eval (assert_eq y (S O)).
Ltac2 mutable quw := fun (n : nat) => O.
Ltac2 Set quw := fun n =>
match n with
| O => O
| S n => S (S (quw n))
end.
Ltac2 Eval (quw (S (S O))).
(** Not the right type *)
Fail Ltac2 Set foo := 0.
Ltac2 bar () := ().
(** Cannot redefine non-mutable tactics *)
Fail Ltac2 Set bar := fun _ => ().
(** Subtype check *)
Ltac2 rec h x := h x.
Ltac2 mutable f x := h x.
Fail Ltac2 Set f := fun x => x.
Ltac2 mutable g x := x.
Ltac2 Set g := h.
(** Rebinding with old values *)
Ltac2 mutable qux n := S n.
Ltac2 Set qux as self := fun n => self (self n).
Ltac2 Eval assert_eq (qux O) (S (S O)).
Ltac2 mutable quz := O.
Ltac2 Set quz as self := S self.
Ltac2 Eval (assert_eq quz (S O)).
Ltac2 rec addn n :=
match n with
| O => fun m => m
| S n => fun m => S (addn n m)
end.
Ltac2 mutable rec quy n :=
match n with
| O => S O
| S n => S (quy n)
end.
Ltac2 Set quy as self := fun n =>
match n with
| O => O
| S n => addn (self n) (quy n)
end.
Ltac2 Eval (assert_eq (quy (S (S O))) (S (S (S O)))).
Ltac2 Eval (assert_eq (quy (S (S (S O)))) (S (S (S (S (S (S O))))))).
|
