diff options
Diffstat (limited to 'theories/Ints/BigZ.v')
| -rw-r--r-- | theories/Ints/BigZ.v | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/theories/Ints/BigZ.v b/theories/Ints/BigZ.v new file mode 100644 index 0000000000..78fe2bced1 --- /dev/null +++ b/theories/Ints/BigZ.v @@ -0,0 +1,19 @@ +Require Export BigN. +Require Import ZMake. + + +Module BigZ := Make BigN. + + +Definition bigZ := BigZ.t. + +Delimit Scope bigZ_scope with bigZ. +Bind Scope bigZ_scope with bigZ. +Bind Scope bigZ_scope with BigZ.t. +Bind Scope bigZ_scope with BigZ.t_. + +Notation " i + j " := (BigZ.add i j) : bigZ_scope. +Notation " i - j " := (BigZ.sub i j) : bigZ_scope. +Notation " i * j " := (BigZ.mul i j) : bigZ_scope. +Notation " i / j " := (BigZ.div i j) : bigZ_scope. +Notation " i ?= j " := (BigZ.compare i j) : bigZ_scope. |