diff options
Diffstat (limited to 'theories')
| -rwxr-xr-x | theories/Init/Datatypes.v | 10 | ||||
| -rwxr-xr-x | theories/Init/Peano.v | 1 |
2 files changed, 10 insertions, 1 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index cb2c272846..8ec5b7c905 100755 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -30,6 +30,10 @@ Add Printing If bool. Inductive nat : Set := O : nat | S : nat->nat. +Delimits Scope nat_scope with N. +Bind Scope nat_scope with nat. +Arguments Scope S [ nat_scope ]. + (** [Empty_set] has no inhabitant *) Inductive Empty_set:Set :=. @@ -46,7 +50,9 @@ Hints Resolve refl_identity : core v62. Inductive option [A:Set] : Set := Some : A -> (option A) | None : (option A). +(* Arguments Scope option [ type_scope ]. +*) (** [sum A B], equivalently [A + B], is the disjoint sum of [A] and [B] *) (* Syntax defined in Specif.v *) @@ -55,7 +61,9 @@ Inductive sum [A,B:Set] : Set | inr : B -> (sum A B). Notation "x + y" := (sum x y) : type_scope. +(* Arguments Scope sum [type_scope type_scope]. +*) (** [prod A B], written [A * B], is the product of [A] and [B]; the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *) @@ -63,7 +71,9 @@ Arguments Scope sum [type_scope type_scope]. Inductive prod [A,B:Set] : Set := pair : A -> B -> (prod A B). Add Printing Let prod. +(* Arguments Scope prod [type_scope type_scope]. +*) Notation "x * y" := (prod x y) : type_scope. Notation "( x , y )" := (pair ? ? x y) V8only "x , y". diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 55e44d28d2..2df5229881 100755 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -199,4 +199,3 @@ Infix NONA 5 ">" gt : nat_scope. V7only [ End nat_scope. ]. -Delimits Scope nat_scope with N. |