package jasmin

  1. Overview
  2. Docs
package jasmin
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Jasmin.Type

type __ = Obj.t
type ltype =
  1. | Coq_lbool
  2. | Coq_lword of Wsize.wsize
val ltype_tag : ltype -> BinNums.positive
type box_ltype_lbool =
  1. | Box_ltype_lbool
type ltype_fields_t = __
val ltype_fields : ltype -> ltype_fields_t
val ltype_eqb_fields : (ltype -> ltype -> bool) -> BinNums.positive -> ltype_fields_t -> ltype_fields_t -> bool
val ltype_eqb : ltype -> ltype -> bool
val ltype_eqb_OK : ltype -> ltype -> Bool.reflect
type atype =
  1. | Coq_abool
  2. | Coq_aint
  3. | Coq_aarr of Wsize.wsize * BinNums.positive
  4. | Coq_aword of Wsize.wsize
val atype_tag : atype -> BinNums.positive
type box_atype_abool =
  1. | Box_atype_abool
type box_atype_aarr = {
  1. coq_Box_atype_aarr_0 : Wsize.wsize;
  2. coq_Box_atype_aarr_1 : BinNums.positive;
}
type atype_fields_t = __
val atype_fields : atype -> atype_fields_t
val atype_eqb_fields : (atype -> atype -> bool) -> BinNums.positive -> atype_fields_t -> atype_fields_t -> bool
val atype_eqb : atype -> atype -> bool
val atype_eqb_OK : atype -> atype -> Bool.reflect
type ctype =
  1. | Coq_cbool
  2. | Coq_cint
  3. | Coq_carr of BinNums.positive
  4. | Coq_cword of Wsize.wsize
val ctype_tag : ctype -> BinNums.positive
type box_ctype_cbool =
  1. | Box_ctype_cbool
type ctype_fields_t = __
val ctype_fields : ctype -> ctype_fields_t
val ctype_eqb_fields : (ctype -> ctype -> bool) -> BinNums.positive -> ctype_fields_t -> ctype_fields_t -> bool
val ctype_eqb : ctype -> ctype -> bool
val ctype_eqb_OK : ctype -> ctype -> Bool.reflect
val atype_of_ltype : ltype -> atype
val ltype_of_atype : atype -> ltype option
val coq_HB_unnamed_factory_1 : ltype Eqtype.Coq_hasDecEq.axioms_
val type_ltype__canonical__eqtype_Equality : Eqtype.Equality.coq_type
val coq_HB_unnamed_factory_3 : atype Eqtype.Coq_hasDecEq.axioms_
val type_atype__canonical__eqtype_Equality : Eqtype.Equality.coq_type
val coq_HB_unnamed_factory_5 : ctype Eqtype.Coq_hasDecEq.axioms_
val type_ctype__canonical__eqtype_Equality : Eqtype.Equality.coq_type
val atype_cmp : atype -> atype -> Datatypes.comparison
module OtherDefs : sig ... end
val eval_atype : atype -> ctype
val eval_ltype : ltype -> ctype
val convertible : atype -> atype -> bool
val subatype : atype -> atype -> bool
val subctype : ctype -> ctype -> bool
type 'len extended_type =
  1. | ETbool
  2. | ETint
  3. | ETarr of Wsize.wsize * 'len
  4. | ETword of Wsize.signedness option * Wsize.wsize
val tbool : 'a1 extended_type
val tint : 'a1 extended_type
val tarr : Wsize.wsize -> 'a1 -> 'a1 extended_type
val tword : Wsize.wsize -> 'a1 extended_type
val tuint : Wsize.wsize -> 'a1 extended_type