Library Coq.Numbers.Natural.BigN.BigN
Natural numbers in base 2^31
Author: Arnaud Spiwack
Module BigN implements NAxiomsSig
Notations about BigN
Notation bigN :=
BigN.t.
Delimit Scope bigN_scope with bigN.
Notation Local "0" :=
BigN.zero :
bigN_scope.
Infix "+" :=
BigN.add :
bigN_scope.
Infix "-" :=
BigN.sub :
bigN_scope.
Infix "*" :=
BigN.mul :
bigN_scope.
Infix "/" :=
BigN.div :
bigN_scope.
Infix "?=" :=
BigN.compare :
bigN_scope.
Infix "==" :=
BigN.eq (
at level 70,
no associativity) :
bigN_scope.
Infix "<" :=
BigN.lt :
bigN_scope.
Infix "<=" :=
BigN.le :
bigN_scope.
Notation "x > y" := (
BigN.lt y x)(
only parsing) :
bigN_scope.
Notation "x >= y" := (
BigN.le y x)(
only parsing) :
bigN_scope.
Notation "[ i ]" := (
BigN.to_Z i) :
bigN_scope.
Open Scope bigN_scope.
Example of reasoning about BigN
BigN is a semi-ring
Todo: tactic translating from BigN to Z + omega
Todo: micromega