Pos (djot.Djot_kernel.PosDef.Pos)

val succ : BinNums.positive -> BinNums.positive

val add : BinNums.positive -> BinNums.positive -> BinNums.positive

val add_carry : BinNums.positive -> BinNums.positive -> BinNums.positive

val pred_double : BinNums.positive -> BinNums.positive

val pred_N : BinNums.positive -> BinNums.coq_N

type mask =

| IsNul
| IsPos of BinNums.positive
| IsNeg

val succ_double_mask : mask -> mask

val double_mask : mask -> mask

val double_pred_mask : BinNums.positive -> mask

val sub_mask : BinNums.positive -> BinNums.positive -> mask

val sub_mask_carry : BinNums.positive -> BinNums.positive -> mask

val mul : BinNums.positive -> BinNums.positive -> BinNums.positive

val iter : ('a1 -> 'a1) -> 'a1 -> BinNums.positive -> 'a1

val compare_cont : 
  Datatypes.comparison ->
  BinNums.positive ->
  BinNums.positive ->
  Datatypes.comparison

val compare : BinNums.positive -> BinNums.positive -> Datatypes.comparison

val eqb : BinNums.positive -> BinNums.positive -> bool

val leb : BinNums.positive -> BinNums.positive -> bool

val sqrtrem_step : 
  (BinNums.positive -> BinNums.positive) ->
  (BinNums.positive -> BinNums.positive) ->
  (BinNums.positive * mask) ->
  BinNums.positive * mask

val sqrtrem : BinNums.positive -> BinNums.positive * mask

val sqrt : BinNums.positive -> BinNums.positive

val coq_Nsucc_double : BinNums.coq_N -> BinNums.coq_N

val coq_Ndouble : BinNums.coq_N -> BinNums.coq_N

val coq_lor : BinNums.positive -> BinNums.positive -> BinNums.positive

val coq_land : BinNums.positive -> BinNums.positive -> BinNums.coq_N

val ldiff : BinNums.positive -> BinNums.positive -> BinNums.coq_N

val coq_lxor : BinNums.positive -> BinNums.positive -> BinNums.coq_N

val iter_op : ('a1 -> 'a1 -> 'a1) -> BinNums.positive -> 'a1 -> 'a1

val to_nat : BinNums.positive -> int

val of_succ_nat : int -> BinNums.positive