From 5dd845375974b2bb2d937f6c05427a92976fa7f1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 5 Nov 2003 23:40:26 +0000
Subject: Notations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4816 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/NArith/BinNat.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 222f6de2fa..4d3d30f212 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -15,6 +15,17 @@ Require BinPos.
 
 Inductive entier: Set := Nul : entier | Pos : positive -> entier.
 
+(** Declare binding key for scope positive_scope *)
+
+Delimits Scope N_scope with N.
+
+(** Automatically open scope N_scope for the constructors of N *)
+
+Bind Scope N_scope with entier.
+Arguments Scope Pos [ N_scope ].
+
+Open Local Scope N_scope.
+
 (** Operation x -> 2*x+1 *)
 
 Definition Un_suivi_de := [x]
@@ -39,6 +50,8 @@ Definition Nplus := [n,m]
   | (Pos p) (Pos q) => (Pos (add p q))
   end.
 
+V8Infix "+" Nplus : N_scope.
+
 (** Multiplication *)
 
 Definition Nmult := [n,m]
@@ -48,6 +61,8 @@ Definition Nmult := [n,m]
   | (Pos p) (Pos q) => (Pos (times p q))
   end.
 
+V8Infix "*" Nmult : N_scope.
+
 (** Order *)
 
 Definition Ncompare := [n,m]
@@ -58,6 +73,8 @@ Definition Ncompare := [n,m]
   | (Pos n') (Pos m') => (compare n' m' EGAL)
   end.
 
+V8Infix "?=" Ncompare (at level 70, no associativity) : N_scope.
+
 (** Peano induction on binary natural numbers *)
 
 Theorem Nind : (P:(entier ->Prop))
-- 
cgit v1.2.3