blob: d003ab323d2c7b93c0808c5bd9ce1798c9429f87 (
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
|
From Ltac2 Require Import Ltac2.
(* true and false are valid constructors even though they are lowercase *)
Ltac2 Eval true.
Ltac2 Eval false.
(* Otherwise constructors have to be Uppercase *)
Ltac2 Type good_constructor := [Uppercased].
Ltac2 Type good_constructors := [Uppercased1 | Uppercased2].
Ltac2 Eval Uppercased2.
Fail Ltac2 Type bad_constructor := [ notUppercased ].
Fail Ltac2 Type bad_constructors := [ | notUppercased1 | notUppercased2 ].
Fail Ltac2 Eval notUppercased2.
(* And the same for open types*)
Ltac2 Type open_type := [ .. ].
Fail Ltac2 Type open_type ::= [ notUppercased3 ].
Ltac2 Type open_type ::= [ Uppercased3 ].
Fail Ltac2 Eval notUppercased3.
Ltac2 Eval Uppercased3.
Fail Ltac2 Type foo ::= [ | bar1 | bar2 ].
|
