# Library Coq.Numbers.BinNums

Set Implicit Arguments.

positive is a datatype representing the strictly positive integers
in a binary way. Starting from 1 (represented by xH), one can
add a new least significant digit via xO (digit 0) or xI (digit 1).
Numbers in positive can also be denoted using a decimal notation;
e.g. 6%positive abbreviates xO (xI xH)

Inductive positive : Set :=

| xI : positive -> positive

| xO : positive -> positive

| xH : positive.

Delimit Scope positive_scope with positive.

N is a datatype representing natural numbers in a binary way,
by extending the positive datatype with a zero.
Numbers in N can also be denoted using a decimal notation;
e.g. 6%N abbreviates Npos (xO (xI xH))

Z is a datatype representing the integers in a binary way.
An integer is either zero or a strictly positive number
(coded as a positive) or a strictly negative number
(whose opposite is stored as a positive value).
Numbers in Z can also be denoted using a decimal notation;
e.g. (-6)%Z abbreviates Zneg (xO (xI xH))