package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val succ : positive -> positive
val add : positive -> positive -> positive
val add_carry : positive -> positive -> positive
val pred_double : positive -> positive
type mask = Pos.mask =
  1. | IsNul
  2. | IsPos of positive
  3. | IsNeg
val succ_double_mask : mask -> mask
val double_mask : mask -> mask
val double_pred_mask : positive -> mask
val sub_mask : positive -> positive -> mask
val sub_mask_carry : positive -> positive -> mask
val sub : positive -> positive -> positive
val mul : positive -> positive -> positive
val iter : ('a1 -> 'a1) -> 'a1 -> positive -> 'a1
val size_nat : positive -> nat
val compare_cont : comparison -> positive -> positive -> comparison
val compare : positive -> positive -> comparison
val max : positive -> positive -> positive
val leb : positive -> positive -> bool
val gcdn : nat -> positive -> positive -> positive
val gcd : positive -> positive -> positive
val of_succ_nat : nat -> positive