blob: a7366f2d35f09a6643e2ce23cf4a14accd17f54d (
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
|
Declare Scope A.
Declare Scope B.
Delimit Scope A with A.
Delimit Scope B with B.
Definition to_unit (v : Number.uint) : option unit
:= match Nat.of_num_uint v with O => Some tt | _ => None end.
Definition of_unit (v : unit) : Number.uint := Nat.to_num_uint 0.
Definition of_unit' (v : unit) : Number.uint := Nat.to_num_uint 1.
Number Notation unit to_unit of_unit : A.
Number Notation unit to_unit of_unit' : B.
Definition f x : unit := x.
Check f tt.
Arguments f x%A.
Check f tt.
Check tt.
Open Scope A.
Check tt.
Close Scope A.
Check tt.
Open Scope B.
Check tt.
Undelimit Scope B.
Check tt.
Open Scope A.
Check tt.
Close Scope A.
Check tt.
Close Scope B.
Check tt.
Open Scope B.
Check tt.
Notation "1" := true.
Check tt.
Open Scope A.
Check tt.
Declare Scope C.
Notation "0" := false : C.
Open Scope C.
Check tt. (* gives 0 but should now be 0%A *)
|
