Library Coq.Numbers.Rational.BigQ.BigQ
We choose for BigQ an implemention with
multiple representation of 0: 0, 1/0, 2/0 etc.
See QMake.v
First, we provide translations functions between BigN and BigZ
This allows to build BigQ out of BigN and BigQ via QMake
Notations about BigQ
Notation bigQ :=
BigQ.t.
Delimit Scope bigQ_scope with bigQ.
Infix "+" :=
BigQ.add :
bigQ_scope.
Infix "-" :=
BigQ.sub :
bigQ_scope.
Notation "- x" := (
BigQ.opp x) :
bigQ_scope.
Infix "*" :=
BigQ.mul :
bigQ_scope.
Infix "/" :=
BigQ.div :
bigQ_scope.
Infix "^" :=
BigQ.power :
bigQ_scope.
Infix "?=" :=
BigQ.compare :
bigQ_scope.
Infix "==" :=
BigQ.eq :
bigQ_scope.
Infix "<" :=
BigQ.lt :
bigQ_scope.
Infix "<=" :=
BigQ.le :
bigQ_scope.
Notation "x > y" := (
BigQ.lt y x)(
only parsing) :
bigQ_scope.
Notation "x >= y" := (
BigQ.le y x)(
only parsing) :
bigQ_scope.
Notation "[ q ]" := (
BigQ.to_Q q) :
bigQ_scope.
Open Scope bigQ_scope.
BigQ is a setoid
BigQ is a field