blob: 07986b0df3360d9e41b2639cdb826ea3f05574d5 (
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
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
|
(* Until recently, the Notation.declare_numeral_notation wasn't synchronized
w.r.t. backtracking. This should be ok now.
This test is pretty artificial (we must declare Z_scope for this to work).
*)
Delimit Scope Z_scope with Z.
Open Scope Z_scope.
Check let v := 0 in v : nat.
(* let v := 0 in v : nat : nat *)
Require BinInt.
Check let v := 0 in v : BinNums.Z.
(* let v := 0 in v : BinNums.Z : BinNums.Z *)
Back 2.
Check let v := 0 in v : nat.
(* Expected answer: let v := 0 in v : nat : nat *)
(* Used to fail with:
Error: Cannot interpret in Z_scope without requiring first module BinNums.
*)
Local Set Universe Polymorphism.
Delimit Scope punit_scope with punit.
Delimit Scope pcunit_scope with pcunit.
Delimit Scope int_scope with int.
Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int : int_scope.
Module A.
NonCumulative Inductive punit@{u} : Type@{u} := ptt.
Cumulative Inductive pcunit@{u} : Type@{u} := pctt.
Definition to_punit : Decimal.int -> option punit
:= fun v => match v with 0%int => Some ptt | _ => None end.
Definition to_pcunit : Decimal.int -> option pcunit
:= fun v => match v with 0%int => Some pctt | _ => None end.
Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0.
Definition of_pcunit : pcunit -> Decimal.uint := fun _ => Nat.to_uint 0.
Numeral Notation punit to_punit of_punit : punit_scope.
Check let v := 0%punit in v : punit.
Back 2.
Numeral Notation pcunit to_pcunit of_pcunit : punit_scope.
Check let v := 0%punit in v : pcunit.
End A.
Reset A.
Local Unset Universe Polymorphism.
Module A.
Inductive punit : Set := ptt.
Definition to_punit : Decimal.int -> option punit
:= fun v => match v with 0%int => Some ptt | _ => None end.
Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0.
Numeral Notation punit to_punit of_punit : punit_scope.
Check let v := 0%punit in v : punit.
End A.
Local Set Universe Polymorphism.
Inductive punit@{u} : Type@{u} := ptt.
Definition to_punit : Decimal.int -> option punit
:= fun v => match v with 0%int => Some ptt | _ => None end.
Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0.
Numeral Notation punit to_punit of_punit : punit_scope.
Check let v := 0%punit in v : punit.
Back 6. (* check backtracking of registering universe polymorphic constants *)
Local Unset Universe Polymorphism.
Inductive punit : Set := ptt.
Definition to_punit : Decimal.int -> option punit
:= fun v => match v with 0%int => Some ptt | _ => None end.
Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0.
Numeral Notation punit to_punit of_punit : punit_scope.
Check let v := 0%punit in v : punit.
|
