package jasmin
Compiler for High-Assurance and High-Speed Cryptography
Install
dune-project
Dependency
Authors
Maintainers
Sources
jasmin-compiler-v2026.03.1.tar.bz2
sha256=78e9f92963403f1ed9f95326f26725532c43956f10fcc47d11ac94c66a236f52
doc/jasmin.jasmin/Jasmin/Choice/index.html
Module Jasmin.Choice
type __ = Obj.tmodule Coq_hasChoice : sig ... endmodule Choice : sig ... endval find_subdef :
Choice.coq_type ->
Choice.sort Ssrbool.pred ->
Datatypes.nat ->
Choice.sort optionval coq_PCanHasChoice :
Choice.coq_type ->
('a1 -> Choice.sort) ->
(Choice.sort -> 'a1 option) ->
'a1 Coq_hasChoice.phant_axiomsval coq_HB_unnamed_factory_6 :
Choice.coq_type ->
('a1 -> Choice.sort) ->
(Choice.sort -> 'a1 option) ->
('a1, Choice.sort) Eqtype.pcan_type Coq_hasChoice.phant_axiomsval nat_hasChoice : Datatypes.nat Coq_hasChoice.phant_axiomsval coq_HB_unnamed_factory_20 : Datatypes.nat Coq_hasChoice.phant_axiomsval coq_Datatypes_nat__canonical__choice_Choice : Choice.coq_typemodule Choice_isCountable : sig ... endmodule Countable : sig ... endval pickle : Countable.coq_type -> Countable.sort -> Datatypes.natval unpickle : Countable.coq_type -> Datatypes.nat -> Countable.sort optionmodule Coq_isCountable : sig ... endmodule Builders_77 : sig ... endval coq_PCanIsCountable :
Countable.coq_type ->
('a1 -> Countable.sort) ->
(Countable.sort -> 'a1 option) ->
'a1 Coq_isCountable.axioms_val coq_HB_unnamed_factory_87 :
Countable.coq_type ->
('a1 -> Countable.sort) ->
(Countable.sort -> 'a1 option) ->
('a1, Countable.sort) Eqtype.pcan_type Coq_isCountable.phant_axiomsval coq_HB_unnamed_mixin_91 :
Countable.coq_type ->
('a1 -> Countable.sort) ->
(Countable.sort -> 'a1 option) ->
('a1, Countable.sort) Eqtype.pcan_type Choice_isCountable.axioms_val eqtype_pcan_type__canonical__choice_Countable :
Countable.coq_type ->
('a1 -> Countable.sort) ->
(Countable.sort -> 'a1 option) ->
Countable.coq_typeval coq_HB_unnamed_mixin_106 :
Countable.coq_type ->
Countable.sort Ssrbool.pred ->
Countable.sort Eqtype.SubType.coq_type ->
Choice.sort Eqtype.SubType.sort Coq_hasChoice.phant_axiomsval coq_HB_unnamed_mixin_107 :
Countable.coq_type ->
Countable.sort Ssrbool.pred ->
Countable.sort Eqtype.SubType.coq_type ->
(Eqtype.Equality.sort Eqtype.SubType.sort, Eqtype.Equality.sort)
Eqtype.inj_type
Eqtype.Coq_hasDecEq.axioms_val coq_HB_unnamed_mixin_109 :
Countable.coq_type ->
Countable.sort Ssrbool.pred ->
Countable.sort Eqtype.SubType.coq_type ->
(Countable.sort Eqtype.SubType.sort, Countable.sort) Eqtype.pcan_type
Choice_isCountable.axioms_val eqtype_sub_type__canonical__choice_Countable :
Countable.coq_type ->
Countable.sort Ssrbool.pred ->
Countable.sort Eqtype.SubType.coq_type ->
Countable.coq_typeval coq_HB_unnamed_factory_120 : Datatypes.nat Choice_isCountable.axioms_val coq_Datatypes_nat__canonical__choice_Countable : Countable.coq_type