summaryrefslogtreecommitdiff
path: root/contrib/setoid_ring/NArithRing.v
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/setoid_ring/NArithRing.v')
-rw-r--r--contrib/setoid_ring/NArithRing.v31
1 files changed, 31 insertions, 0 deletions
diff --git a/contrib/setoid_ring/NArithRing.v b/contrib/setoid_ring/NArithRing.v
new file mode 100644
index 00000000..33e3cb4e
--- /dev/null
+++ b/contrib/setoid_ring/NArithRing.v
@@ -0,0 +1,31 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+Require Export Ring.
+Require Import BinPos BinNat.
+Import InitialRing.
+
+Set Implicit Arguments.
+
+Ltac isNcst t :=
+ let t := eval hnf in t in
+ match t with
+ N0 => constr:true
+ | Npos ?p => isNcst p
+ | xI ?p => isNcst p
+ | xO ?p => isNcst p
+ | xH => constr:true
+ | _ => constr:false
+ end.
+Ltac Ncst t :=
+ match isNcst t with
+ true => t
+ | _ => NotConstant
+ end.
+
+Add Ring Nr : Nth (decidable Neq_bool_ok, constants [Ncst]).