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
|
Require Import Ltac2.Ltac2.
(** Ltac2 is typed à la ML. *)
Ltac2 test0 n := Int.add n 1.
Print Ltac2 test0.
Ltac2 test1 () := test0 0.
Print Ltac2 test1.
Fail Ltac2 test2 () := test0 true.
Fail Ltac2 test2 () := test0 0 0.
Ltac2 test3 f x := x, (f x, x).
Print Ltac2 test3.
(** Polymorphism *)
Ltac2 rec list_length l :=
match l with
| [] => 0
| x :: l => Int.add 1 (list_length l)
end.
Print Ltac2 list_length.
(** Pattern-matching *)
Ltac2 ifb b f g := match b with
| true => f ()
| false => g ()
end.
Print Ltac2 ifb.
Ltac2 if_not_found e f g := match e with
| Not_found => f ()
| _ => g ()
end.
Fail Ltac2 ifb' b f g := match b with
| true => f ()
end.
Fail Ltac2 if_not_found' e f g := match e with
| Not_found => f ()
end.
(** Reimplementing 'do'. Return value of the function useless. *)
Ltac2 rec do n tac := match Int.equal n 0 with
| true => ()
| false => tac (); do (Int.sub n 1) tac
end.
Print Ltac2 do.
(** Non-function pure values are OK. *)
Ltac2 tuple0 := ([1; 2], true, (fun () => "yay")).
Print Ltac2 tuple0.
(** Impure values are not. *)
Fail Ltac2 not_a_value := { contents := 0 }.
Fail Ltac2 not_a_value := "nope".
Fail Ltac2 not_a_value := list_length [].
|
