package jasmin

  1. Overview
  2. Docs

Module Jasmin.Utils0

type __ = Obj.t
module FinIsCount : sig ... end
type 't eqTypeC = {
  1. beq : 't -> 't -> bool;
  2. ceqP : 't Eqtype.eq_axiom;
}
val beq : 'a1 eqTypeC -> 'a1 -> 'a1 -> bool
val ceqP : 'a1 eqTypeC -> 'a1 Eqtype.eq_axiom
module EqType : sig ... end
val ceqT_eqType : 'a1 eqTypeC -> Eqtype.Equality.coq_type
type 't finTypeC = {
  1. _eqC : 't eqTypeC;
  2. cenum : 't list;
}
val _eqC : 'a1 finTypeC -> 'a1 eqTypeC
val cenum : 'a1 finTypeC -> 'a1 list
module FinType : sig ... end
val cfinT_finType : 'a1 finTypeC -> Fintype.Finite.coq_type
module FinMap : sig ... end
type ('e, 'a) result =
  1. | Ok of 'a
  2. | Error of 'e
val is_ok : ('a1, 'a2) result -> bool
val is_okP : ('a1, 'a2) result -> Datatypes.reflect
module Result : sig ... end
val o2r : 'a1 -> 'a2 option -> ('a1, 'a2) result
val coq_assert : bool -> 'a1 -> ('a1, unit) result
type assertion_label = string
type error =
  1. | ErrOob
  2. | ErrAddrUndef
  3. | ErrAddrInvalid
  4. | ErrStack
  5. | ErrType
  6. | ErrArith
  7. | ErrSemUndef
  8. | ErrAssert of assertion_label
type 't exec = (error, 't) result
val type_error : (error, 'a1) result
val undef_error : (error, 'a1) result
val rbindP : ('a1, 'a2) result -> ('a2 -> ('a1, 'a3) result) -> 'a3 -> ('a2 -> __ -> __ -> 'a4) -> 'a4
val mapM : ('a2 -> ('a1, 'a3) result) -> 'a2 list -> ('a1, 'a3 list) result
val foldM : ('a2 -> 'a3 -> ('a1, 'a3) result) -> 'a3 -> 'a2 list -> ('a1, 'a3) result
val fold2 : 'a3 -> ('a1 -> 'a2 -> 'a4 -> ('a3, 'a4) result) -> 'a1 list -> 'a2 list -> 'a4 -> ('a3, 'a4) result
val allM : ('a1 -> ('a2, unit) result) -> 'a1 list -> ('a2, unit) result
val mapM2 : 'a3 -> ('a1 -> 'a2 -> ('a3, 'a4) result) -> 'a1 list -> 'a2 list -> ('a3, 'a4 list) result
val fmap : ('a1 -> 'a2 -> 'a1 * 'a3) -> 'a1 -> 'a2 list -> 'a1 * 'a3 list
val fmapM : ('a2 -> 'a3 -> ('a1, 'a2 * 'a4) result) -> 'a2 -> 'a3 list -> ('a1, 'a2 * 'a4 list) result
val fmapM2 : 'a1 -> ('a2 -> 'a3 -> 'a4 -> ('a1, 'a2 * 'a5) result) -> 'a2 -> 'a3 list -> 'a4 list -> ('a1, 'a2 * 'a5 list) result
val all2P : ('a1 -> 'a2 -> bool) -> 'a1 list -> 'a2 list -> Datatypes.reflect
val reflect_all2_eqb : ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> Datatypes.reflect) -> 'a1 list -> 'a1 list -> Datatypes.reflect
val map2 : ('a1 -> 'a2 -> 'a3) -> 'a1 list -> 'a2 list -> 'a3 list
val map3 : ('a1 -> 'a2 -> 'a3 -> 'a4) -> 'a1 list -> 'a2 list -> 'a3 list -> 'a4 list
val mapi_aux : (Datatypes.nat -> 'a1 -> 'a2) -> Datatypes.nat -> 'a1 list -> 'a2 list
val mapi : (Datatypes.nat -> 'a1 -> 'a2) -> 'a1 list -> 'a2 list
val find_map : ('a1 -> 'a2 option) -> 'a1 list -> 'a2 option
val isSome_obind : ('a1 -> 'a2 option) -> 'a1 option -> Datatypes.reflect
val coq_HB_unnamed_factory_14 : Datatypes.comparison Eqtype.Coq_hasDecEq.axioms_
val coq_Datatypes_comparison__canonical__eqtype_Equality : Eqtype.Equality.coq_type
val gcmp : ('a1 -> 'a1 -> Datatypes.comparison) -> 'a1 -> 'a1 -> Datatypes.comparison
val cmp_lt : ('a1 -> 'a1 -> Datatypes.comparison) -> 'a1 -> 'a1 -> bool
val cmp_le : ('a1 -> 'a1 -> Datatypes.comparison) -> 'a1 -> 'a1 -> bool
val lex : ('a1 -> 'a1 -> Datatypes.comparison) -> ('a2 -> 'a2 -> Datatypes.comparison) -> ('a1 * 'a2) -> ('a1 * 'a2) -> Datatypes.comparison
val cmp_min : ('a1 -> 'a1 -> Datatypes.comparison) -> 'a1 -> 'a1 -> 'a1
val cmp_max : ('a1 -> 'a1 -> Datatypes.comparison) -> 'a1 -> 'a1 -> 'a1
val bool_cmp : bool -> bool -> Datatypes.comparison
val subrelation_iff_flip_arrow : (__, __) CRelationClasses.iffT -> (__, __) CRelationClasses.arrow
val reflect_m : bool -> bool -> (__, __) CRelationClasses.iffT
type is_positive =
  1. | Coq_is_xI of BinNums.positive * is_positive
  2. | Coq_is_xO of BinNums.positive * is_positive
  3. | Coq_is_xH
val is_positive_rect : (BinNums.positive -> is_positive -> 'a1 -> 'a1) -> (BinNums.positive -> is_positive -> 'a1 -> 'a1) -> 'a1 -> BinNums.positive -> is_positive -> 'a1
val is_positive_rec : (BinNums.positive -> is_positive -> 'a1 -> 'a1) -> (BinNums.positive -> is_positive -> 'a1 -> 'a1) -> 'a1 -> BinNums.positive -> is_positive -> 'a1
val positive_tag : BinNums.positive -> BinNums.positive
val is_positive_inhab : BinNums.positive -> is_positive
val is_positive_functor : BinNums.positive -> is_positive -> is_positive
type box_positive_xI = BinNums.positive
val coq_Box_positive_xI_0 : box_positive_xI -> BinNums.positive
type box_positive_xH =
  1. | Box_positive_xH
type positive_fields_t = __
val positive_fields : BinNums.positive -> positive_fields_t
val positive_construct : BinNums.positive -> positive_fields_t -> BinNums.positive option
val positive_induction : (BinNums.positive -> 'a1 -> 'a1) -> (BinNums.positive -> 'a1 -> 'a1) -> 'a1 -> BinNums.positive -> is_positive -> 'a1
val positive_eqb_fields : (BinNums.positive -> BinNums.positive -> bool) -> BinNums.positive -> positive_fields_t -> positive_fields_t -> bool
val positive_eqb : BinNums.positive -> BinNums.positive -> bool
val positive_eqb_OK_sumbool : BinNums.positive -> BinNums.positive -> bool
type is_Z =
  1. | Coq_is_Z0
  2. | Coq_is_Zpos of BinNums.positive * is_positive
  3. | Coq_is_Zneg of BinNums.positive * is_positive
val is_Z_rect : 'a1 -> (BinNums.positive -> is_positive -> 'a1) -> (BinNums.positive -> is_positive -> 'a1) -> BinNums.coq_Z -> is_Z -> 'a1
val is_Z_rec : 'a1 -> (BinNums.positive -> is_positive -> 'a1) -> (BinNums.positive -> is_positive -> 'a1) -> BinNums.coq_Z -> is_Z -> 'a1
val coq_Z_tag : BinNums.coq_Z -> BinNums.positive
val is_Z_inhab : BinNums.coq_Z -> is_Z
val is_Z_functor : BinNums.coq_Z -> is_Z -> is_Z
type box_Z_Z0 =
  1. | Box_Z_Z0
type box_Z_Zpos = BinNums.positive
val coq_Box_Z_Zpos_0 : box_Z_Zpos -> BinNums.positive
type coq_Z_fields_t = __
val coq_Z_fields : BinNums.coq_Z -> coq_Z_fields_t
val coq_Z_construct : BinNums.positive -> coq_Z_fields_t -> BinNums.coq_Z option
val coq_Z_induction : 'a1 -> (BinNums.positive -> is_positive -> 'a1) -> (BinNums.positive -> is_positive -> 'a1) -> BinNums.coq_Z -> is_Z -> 'a1
val coq_Z_eqb_fields : (BinNums.coq_Z -> BinNums.coq_Z -> bool) -> BinNums.positive -> coq_Z_fields_t -> coq_Z_fields_t -> bool
val coq_Z_eqb : BinNums.coq_Z -> BinNums.coq_Z -> bool
val coq_Z_eqb_OK_sumbool : BinNums.coq_Z -> BinNums.coq_Z -> bool
val coq_HB_unnamed_factory_16 : BinNums.positive Eqtype.Coq_hasDecEq.axioms_
val coq_BinNums_positive__canonical__eqtype_Equality : Eqtype.Equality.coq_type
val ziota_rec : BinNums.coq_Z -> BinNums.coq_Z -> BinNums.coq_Z list
val pnth : 'a1 -> 'a1 list -> BinNums.positive -> 'a1
val znth : 'a1 -> 'a1 list -> BinNums.coq_Z -> 'a1
type 'tr lprod = __
type ltuple = __
val merge_tuple : __ list -> __ list -> ltuple -> ltuple -> ltuple
val obindP : 'a1 option -> ('a1 -> 'a2 option) -> 'a2 -> ('a1 -> __ -> __ -> 'a3) -> 'a3
val oassert : bool -> unit option