diff options
Diffstat (limited to 'theories/Numbers/Rational/BigQ/BigQ.v')
| -rw-r--r-- | theories/Numbers/Rational/BigQ/BigQ.v | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v new file mode 100644 index 00000000..39e120f7 --- /dev/null +++ b/theories/Numbers/Rational/BigQ/BigQ.v @@ -0,0 +1,35 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: BigQ.v 11028 2008-06-01 17:34:19Z letouzey $ i*) + +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 <: QSig.QType := Q0. + +Notation 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. |