package jasmin
Compiler for High-Assurance and High-Speed Cryptography
Install
dune-project
Dependency
Authors
Maintainers
Sources
jasmin-compiler-v2026.09.0.tar.bz2
sha256=11fec571efb9f7b3a47fea324b4e2a68289e0b73b2248d237eccf139b5218190
doc/jasmin.jasmin/Jasmin/BinInt/Z/index.html
Module BinInt.Z
val double : BinNums.coq_Z -> BinNums.coq_Zval succ_double : BinNums.coq_Z -> BinNums.coq_Zval pred_double : BinNums.coq_Z -> BinNums.coq_Zval pos_sub : BinNums.positive -> BinNums.positive -> BinNums.coq_Zval add : BinNums.coq_Z -> BinNums.coq_Z -> BinNums.coq_Zval opp : BinNums.coq_Z -> BinNums.coq_Zval sub : BinNums.coq_Z -> BinNums.coq_Z -> BinNums.coq_Zval mul : BinNums.coq_Z -> BinNums.coq_Z -> BinNums.coq_Zval pow_pos : BinNums.coq_Z -> BinNums.positive -> BinNums.coq_Zval pow : BinNums.coq_Z -> BinNums.coq_Z -> BinNums.coq_Zval compare : BinNums.coq_Z -> BinNums.coq_Z -> Datatypes.comparisonval leb : BinNums.coq_Z -> BinNums.coq_Z -> boolval ltb : BinNums.coq_Z -> BinNums.coq_Z -> boolval eqb : BinNums.coq_Z -> BinNums.coq_Z -> boolval max : BinNums.coq_Z -> BinNums.coq_Z -> BinNums.coq_Zval min : BinNums.coq_Z -> BinNums.coq_Z -> BinNums.coq_Zval to_nat : BinNums.coq_Z -> Datatypes.natval of_nat : Datatypes.nat -> BinNums.coq_Zval of_N : BinNums.coq_N -> BinNums.coq_Zval pos_div_eucl :
BinNums.positive ->
BinNums.coq_Z ->
BinNums.coq_Z * BinNums.coq_Zval div_eucl : BinNums.coq_Z -> BinNums.coq_Z -> BinNums.coq_Z * BinNums.coq_Zval div : BinNums.coq_Z -> BinNums.coq_Z -> BinNums.coq_Zval modulo : BinNums.coq_Z -> BinNums.coq_Z -> BinNums.coq_Zval quotrem : BinNums.coq_Z -> BinNums.coq_Z -> BinNums.coq_Z * BinNums.coq_Zval quot : BinNums.coq_Z -> BinNums.coq_Z -> BinNums.coq_Zval rem : BinNums.coq_Z -> BinNums.coq_Z -> BinNums.coq_Zval div2 : BinNums.coq_Z -> BinNums.coq_Zval shiftl : BinNums.coq_Z -> BinNums.coq_Z -> BinNums.coq_Zval shiftr : BinNums.coq_Z -> BinNums.coq_Z -> BinNums.coq_Zval coq_lor : BinNums.coq_Z -> BinNums.coq_Z -> BinNums.coq_Zval coq_land : BinNums.coq_Z -> BinNums.coq_Z -> BinNums.coq_Zval coq_lxor : BinNums.coq_Z -> BinNums.coq_Z -> BinNums.coq_Zval succ : BinNums.coq_Z -> BinNums.coq_Zval pred : BinNums.coq_Z -> BinNums.coq_Zval geb : BinNums.coq_Z -> BinNums.coq_Z -> boolval gtb : BinNums.coq_Z -> BinNums.coq_Z -> boolval abs : BinNums.coq_Z -> BinNums.coq_Zval odd : BinNums.coq_Z -> boolval log2 : BinNums.coq_Z -> BinNums.coq_Zval testbit : BinNums.coq_Z -> BinNums.coq_Z -> boolval eq_dec : BinNums.coq_Z -> BinNums.coq_Z -> boolval leb_spec0 : BinNums.coq_Z -> BinNums.coq_Z -> Datatypes.reflectval ltb_spec0 : BinNums.coq_Z -> BinNums.coq_Z -> Datatypes.reflectval b2z : bool -> BinNums.coq_Zval lnot : BinNums.coq_Z -> BinNums.coq_Z