|
(* 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.
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
