diff options
Diffstat (limited to 'theories/Numbers/Rational/BigQ/BigQ.v')
| -rw-r--r-- | theories/Numbers/Rational/BigQ/BigQ.v | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v new file mode 100644 index 0000000000..33e5f669cd --- /dev/null +++ b/theories/Numbers/Rational/BigQ/BigQ.v @@ -0,0 +1,32 @@ +(************************************************************************) +(* 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 QMake_base. +Require Import QpMake. +Require Import QvMake. +Require Import Q0Make. +Require Import QifMake. +Require Import QbiMake. + +(* We choose for Q the implemention with + multiple representation of 0: 0, 1/0, 2/0 etc *) +Module BigQ := Q0. + +Definition bigQ := BigQ.t. + +Delimit Scope bigQ_scope with bigQ. +Bind Scope bigQ_scope with bigQ. +Bind Scope bigQ_scope with BigQ.t. + +Notation " i + j " := (BigQ.add i j) : bigQ_scope. +Notation " i - j " := (BigQ.sub i j) : bigQ_scope. +Notation " i * j " := (BigQ.mul i j) : bigQ_scope. +Notation " i / j " := (BigQ.div i j) : bigQ_scope. +Notation " i ?= j " := (BigQ.compare i j) : bigQ_scope. |