blob: 8460ab42b7af3828c86345f6097bd19e39f30469 (
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
|
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.
(** Polymorphism *)
Ltac2 rec list_length l :=
match l with
| [] => 0
| x :: l => Int.add 1 (list_length l)
end.
Print Ltac2 list_length.
|
