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
|
Require Import Ltac2.Init.
Ltac2 @ external type : constr -> constr := "coq-core.plugins.ltac2" "constr_type".
Print Ltac2 Signatures.
Print type.
Locate type.
About type.
(* constructors *)
Print Ltac2 None.
Print Ltac2 Some.
Print Err.
Ltac2 Type ('a,'b) either := [ Inl ('a) | Inr ('b) ].
Print Ltac2 Inl.
Print Ltac2 Inr.
Ltac2 Type ('a,'b,'c) triple := [ Triple ('c, 'b, 'a) ].
Print Ltac2 Triple.
Print Ltac2 Not_found.
Print Ltac2 Out_of_bounds.
(* alias *)
Ltac2 Notation nota := () ().
Print nota.
(* types *)
Print constr.
Ltac2 Type constr := constr.
Print constr.
Ltac2 Type ('a,'b) thing := 'b option.
Print Ltac2 Type thing.
Ltac2 Type empty := [].
Print empty.
Print Ltac2 Type option.
Print Ltac2 Type bool.
Print triple.
Print ref.
Ltac2 Type ('a,'b,'c) trirecord := { cproj : 'c; mutable bproj : 'b; aproj : 'a }.
Print trirecord.
Ltac2 Type extensible := [ .. ].
Print extensible.
Ltac2 Type extensible ::= [ Thing (string) ].
Ltac2 Type extensible ::= [ OtherThing (bool) ].
Print extensible.
|
