package jasmin
Compiler for High-Assurance and High-Speed Cryptography
Install
dune-project
Dependency
Authors
Maintainers
Sources
jasmin-compiler-v2026.03.0.tar.bz2
sha256=dec62a3cd0cd42cfe96ec64b3cd3961e0e8a09fb92ceb64175cffb54fde50e40
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 succ : BinNums.coq_Z -> BinNums.coq_Zval pred : 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 geb : BinNums.coq_Z -> BinNums.coq_Z -> boolval gtb : 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 abs : 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 to_pos : BinNums.coq_Z -> BinNums.positiveval 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 odd : BinNums.coq_Z -> boolval div2 : BinNums.coq_Z -> BinNums.coq_Zval log2 : BinNums.coq_Z -> BinNums.coq_Zval testbit : BinNums.coq_Z -> BinNums.coq_Z -> boolval 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 eq_dec : BinNums.coq_Z -> BinNums.coq_Z -> boolval leb_spec0 : BinNums.coq_Z -> BinNums.coq_Z -> Bool.reflectval ltb_spec0 : BinNums.coq_Z -> BinNums.coq_Z -> Bool.reflectval b2z : bool -> BinNums.coq_Zval lnot : BinNums.coq_Z -> BinNums.coq_Z