package jasmin
Compiler for High-Assurance and High-Speed Cryptography
Install
dune-project
Dependency
Authors
Maintainers
Sources
jasmin-compiler-v2025.06.1.tar.bz2
sha256=e92b42fa69da7c730b0c26dacf842a72b4febcaf4f2157a1dc18b3cce1f859fa
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