Infix "++" := app (right associativity, at level 60) : list_scope.
*)
-(* From Num/Leibniz/EqAxioms **********************************************)
-
-(* NOTATION
-Grammar constr constr1 :=
-eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ].
-*)
-
-(* NOTATION
-Syntax constr
- level 1:
- equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "=" $t2:E ] ].
-*)
-
-(* From Num/Leibniz/NSyntax ***********************************************)
-
-(* NOTATION
-Infix 6 "<" lt.
-*)
-
-(* NOTATION
-Infix 6 "<=" le.
-*)
-
-(* NOTATION
-Infix 6 ">" gt.
-*)
-
-(* NOTATION
-Infix 6 ">=" ge.
-*)
-
-(* NOTATION
-Grammar constr lassoc_constr4 :=
- squash_sum
- [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
- case [$c2] of
- (SQUASH $T2) ->
- case [$c1] of
- (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
- | $_ -> [ (sumor $c1 $T2) ] (* c1+{T2} *)
- esac
- | $_ -> [ (add $c1 $c2) ] (* c1+c2 *)
- esac.
-*)
-
-(* NOTATION
-Syntax constr
- level 1:
- equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "=" $t2:E ] ]
- ;
-
- level 4:
- sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
-.
-*)
-
-(* From Num/Nat/NSyntax ***************************************************)
-
-(* NOTATION
-Infix 6 "<" lt.
-*)
-
-(* NOTATION
-Infix 6 "<=" le.
-*)
-
-(* NOTATION
-Infix 6 ">" gt.
-*)
-
-(* NOTATION
-Infix 6 ">=" ge.
-*)
-
-(* NOTATION
-Grammar constr lassoc_constr4 :=
- squash_sum
- [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
- case [$c2] of
- (SQUASH $T2) ->
- case [$c1] of
- (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
- | $_ -> [ (sumor $c1 $T2) ] (* c1+{T2} *)
- esac
- | $_ -> [ (add $c1 $c2) ] (* c1+c2 *)
- esac.
-*)
-
-(* NOTATION
-Syntax constr
- level 4:
- sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
-.
-*)
-
-(* From Num/EqParams ******************************************************)
+(* From NArith/BinNat *****************************************************)
(* NOTATION
-Grammar constr constr1 :=
-eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ].
+Infix "+" := Nplus : N_scope.
*)
(* NOTATION
-Syntax constr
- level 1:
- equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "=" $t2:E ] ]
-.
-*)
-
-(* From Num/NSyntax *******************************************************)
-
-(* NOTATION
-Infix 6 "<" lt V8only 70.
+Infix "*" := Nmult : N_scope.
*)
(* NOTATION
-Infix 6 "<=" le V8only 70.
+Infix "?=" := Ncompare (at level 70, no associativity) : N_scope.
*)
-(* NOTATION
-Infix 6 ">" gt V8only 70.
-*)
+(* From NArith/BinPos *****************************************************)
(* NOTATION
-Infix 6 ">=" ge V8only 70.
+Infix "+" := Pplus : positive_scope.
*)
(* NOTATION
-Grammar constr lassoc_constr4 :=
- squash_sum
- [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
- case [$c2] of
- (SQUASH $T2) ->
- case [$c1] of
- (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
- | $_ -> [ (sumor $c1 $T2) ] (* c1+{T2} *)
- esac
- | $_ -> [ (add $c1 $c2) ] (* c1+c2 *)
- esac.
+Infix "-" := Pminus : positive_scope.
*)
(* NOTATION
-Syntax constr
- level 4:
- sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
-.
+Infix "*" := Pmult : positive_scope.
*)
-(* From Num/NeqDef ********************************************************)
-
(* NOTATION
-Infix 6 "<>" neq V8only 70.
+Infix "/" := Pdiv2 : positive_scope.
*)
-(* From Num/NeqParams *****************************************************)
-
(* NOTATION
-Infix 6 "<>" neq V8only 70.
+Infix "?=" := Pcompare (at level 70, no associativity) : positive_scope.
*)
(* From Reals/RIneq *******************************************************)
Notation Le_AsB := (le_AsB A B leA leB).
*)
-(* From Wellfounded/Lexicographic_Product *********************************)
-
-(* NOTATION
-Notation LexProd := (lexprod A B leA leB).
-*)
-
-(* NOTATION
-Notation Symprod := (symprod A B leA leB).
-*)
-
-(* NOTATION
-Notation SwapProd := (swapprod A R).
-*)
-
-(* From Wellfounded/Union *************************************************)
-
-(* NOTATION
-Notation Union := (union A R1 R2).
-*)
-
(* From Wellfounded/Lexicographic_Exponentiation **************************)
(* NOTATION
Notation "<< x , y >>" := (exist Descl x y) (at level 0, x, y at level 100).
*)
-(* From Wellfounded/Transitive_Closure ************************************)
+(* From Wellfounded/Lexicographic_Product *********************************)
(* NOTATION
-Notation trans_clos := (clos_trans A R).
+Notation LexProd := (lexprod A B leA leB).
*)
-(* From ZArith/Zdiv *******************************************************)
-
(* NOTATION
-Infix "/" := Zdiv : Z_scope.
+Notation Symprod := (symprod A B leA leB).
*)
(* NOTATION
-Infix "mod" := Zmod (at level 40, no associativity) : Z_scope.
+Notation SwapProd := (swapprod A R).
*)
-(* From ZArith/Zpower *****************************************************)
+(* From Wellfounded/Transitive_Closure ************************************)
(* NOTATION
-Infix "^" := Zpower : Z_scope.
+Notation trans_clos := (clos_trans A R).
*)
+(* From Wellfounded/Union *************************************************)
+
(* NOTATION
-Infix "^" := Zpower : Z_scope.
+Notation Union := (union A R1 R2).
*)
(* From ZArith/BinInt *****************************************************)
Notation "x < y <= z" := (x < y /\ y <= z) : Z_scope.
*)
-(* From ZArith/Znumtheory *************************************************)
-
-(* NOTATION
-Notation "( a | b )" := (Zdivide a b) (at level 0) : Z_scope.
-*)
-
-(* From NArith/BinNat *****************************************************)
-
-(* NOTATION
-Infix "+" := Nplus : N_scope.
-*)
+(* From ZArith/Zdiv *******************************************************)
(* NOTATION
-Infix "*" := Nmult : N_scope.
+Infix "/" := Zdiv : Z_scope.
*)
(* NOTATION
-Infix "?=" := Ncompare (at level 70, no associativity) : N_scope.
+Infix "mod" := Zmod (at level 40, no associativity) : Z_scope.
*)
-(* From NArith/BinPos *****************************************************)
-
-(* NOTATION
-Infix "+" := Pplus : positive_scope.
-*)
+(* From ZArith/Znumtheory *************************************************)
(* NOTATION
-Infix "-" := Pminus : positive_scope.
+Notation "( a | b )" := (Zdivide a b) (at level 0) : Z_scope.
*)
-(* NOTATION
-Infix "*" := Pmult : positive_scope.
-*)
+(* From ZArith/Zpower *****************************************************)
(* NOTATION
-Infix "/" := Pdiv2 : positive_scope.
+Infix "^" := Zpower : Z_scope.
*)
(* NOTATION
-Infix "?=" := Pcompare (at level 70, no associativity) : positive_scope.
+Infix "^" := Zpower : Z_scope.
*)