package jasmin

  1. Overview
  2. Docs
Compiler for High-Assurance and High-Speed Cryptography

Install 

dune-project
 Dependency

github.com Readme Edit opam file Versions (23)

Authors

  1. J
    Jasmin authors and contributors

Maintainers

  1. J
    Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr>

Sources

jasmin-compiler-v2026.09.0.tar.bz2
sha256=11fec571efb9f7b3a47fea324b4e2a68289e0b73b2248d237eccf139b5218190

doc/jasmin.jasmin/Jasmin/Type/index.html

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 -> Datatypes.reflect
type atype =
  1. | Coq_abool
  2. | Coq_aint
  3. | Coq_aarr of Wsize.wsize * BinNums.coq_Z
  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.coq_Z;
}
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 -> Datatypes.reflect
type ctype =
  1. | Coq_cbool
  2. | Coq_cint
  3. | Coq_carr of BinNums.coq_Z
  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 -> Datatypes.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 extended_type_tag : 'a1 extended_type -> BinNums.positive
type 'a box_extended_type_ETbool =
  1. | Box_extended_type_ETbool
type 'a box_extended_type_ETarr = {
  1. coq_Box_extended_type_ETarr_0 : Wsize.wsize;
  2. coq_Box_extended_type_ETarr_1 : 'a;
}
type 'a box_extended_type_ETword = {
  1. coq_Box_extended_type_ETword_0 : Wsize.signedness option;
  2. coq_Box_extended_type_ETword_1 : Wsize.wsize;
}
type 'p extended_type_fields_t = __
val extended_type_fields : 'a1 extended_type -> 'a1 extended_type_fields_t
val extended_type_eqb_fields : ('a1 -> 'a1 -> bool) -> ('a1 extended_type -> 'a1 extended_type -> bool) -> BinNums.positive -> 'a1 extended_type_fields_t -> 'a1 extended_type_fields_t -> bool
val extended_type_eqb : ('a1 -> 'a1 -> bool) -> 'a1 extended_type -> 'a1 extended_type -> bool
val extended_type_eqb_OK : ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> Datatypes.reflect) -> 'a1 extended_type -> 'a1 extended_type -> Datatypes.reflect
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
val type_extended_type__canonical__eqtype_Equality : Eqtype.Equality.coq_type -> Eqtype.Equality.coq_type