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/Choice/index.html
Module Jasmin.Choice
type __ = Obj.tmodule CodeSeq : sig ... endval tag_of_pair : ('a1 * 'a2) -> ('a1, 'a2) Specif.sigTval pair_of_tag : ('a1, 'a2) Specif.sigT -> 'a1 * 'a2val opair_of_sum : ('a1, 'a2) Datatypes.sum -> 'a1 option * 'a2 optionval sum_of_opair : ('a1 option * 'a2 option) -> ('a1, 'a2) Datatypes.sum optionmodule 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 eqtype_pcan_type__canonical__choice_Choice :
Choice.coq_type ->
('a1 -> Choice.sort) ->
(Choice.sort -> 'a1 option) ->
Choice.coq_typeval coq_HB_unnamed_factory_9 :
Choice.coq_type ->
('a1 -> Choice.sort) ->
(Choice.sort -> 'a1) ->
('a1, Choice.sort) Eqtype.can_type Coq_hasChoice.phant_axiomsval eqtype_can_type__canonical__choice_Choice :
Choice.coq_type ->
('a1 -> Choice.sort) ->
(Choice.sort -> 'a1) ->
Choice.coq_typeval seq_hasChoice :
Choice.coq_type ->
Choice.sort list Coq_hasChoice.phant_axiomsval coq_HB_unnamed_factory_16 :
Choice.coq_type ->
Choice.sort list Coq_hasChoice.phant_axiomsval coq_Datatypes_list__canonical__choice_Choice :
Choice.coq_type ->
Choice.coq_typeval tagged_hasChoice :
Choice.coq_type ->
(Choice.sort -> Choice.coq_type) ->
(Choice.sort, Choice.sort) Specif.sigT Coq_hasChoice.phant_axiomsval coq_HB_unnamed_factory_18 :
Choice.coq_type ->
(Choice.sort -> Choice.coq_type) ->
(Choice.sort, Choice.sort) Specif.sigT Coq_hasChoice.phant_axiomsval coq_Specif_sigT__canonical__choice_Choice :
Choice.coq_type ->
(Choice.sort -> Choice.coq_type) ->
Choice.coq_typeval 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_typeval coq_HB_unnamed_factory_43 :
Choice.coq_type ->
Choice.sort option Choice.axioms_val coq_HB_unnamed_mixin_48 :
Choice.coq_type ->
Choice.sort option Coq_hasChoice.axioms_val coq_Datatypes_option__canonical__choice_Choice :
Choice.coq_type ->
Choice.coq_typeval coq_HB_unnamed_factory_50 :
Choice.coq_type ->
Choice.coq_type ->
(Choice.sort * Choice.sort) Choice.axioms_val coq_HB_unnamed_mixin_55 :
Choice.coq_type ->
Choice.coq_type ->
(Choice.sort * Choice.sort) Coq_hasChoice.axioms_val coq_Datatypes_prod__canonical__choice_Choice :
Choice.coq_type ->
Choice.coq_type ->
Choice.coq_typeval coq_HB_unnamed_factory_57 :
Choice.coq_type ->
Choice.coq_type ->
(Choice.sort, Choice.sort) Datatypes.sum Choice.axioms_val coq_HB_unnamed_mixin_62 :
Choice.coq_type ->
Choice.coq_type ->
(Choice.sort, Choice.sort) Datatypes.sum Coq_hasChoice.axioms_module 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_CanIsCountable :
Countable.coq_type ->
('a1 -> Countable.sort) ->
(Countable.sort -> 'a1) ->
'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_factory_93 :
Countable.coq_type ->
('a1 -> Countable.sort) ->
(Countable.sort -> 'a1) ->
('a1, Countable.sort) Eqtype.can_type Coq_isCountable.phant_axiomsval coq_HB_unnamed_mixin_100 :
Countable.coq_type ->
('a1 -> Countable.sort) ->
(Countable.sort -> 'a1) ->
('a1, Countable.sort) Eqtype.can_type Choice_isCountable.axioms_val eqtype_can_type__canonical__choice_Countable :
Countable.coq_type ->
('a1 -> Countable.sort) ->
(Countable.sort -> 'a1) ->
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 pickle_seq : Countable.coq_type -> Countable.sort list -> Datatypes.natval unpickle_seq :
Countable.coq_type ->
Datatypes.nat ->
Countable.sort list optionval coq_HB_unnamed_factory_110 :
Countable.coq_type ->
Countable.sort list Coq_isCountable.axioms_val coq_HB_unnamed_mixin_117 :
Countable.coq_type ->
Countable.sort list Choice_isCountable.axioms_val coq_Datatypes_list__canonical__choice_Countable :
Countable.coq_type ->
Countable.coq_typeval pickle_tagged :
Countable.coq_type ->
(Countable.sort -> Countable.coq_type) ->
(Countable.sort, Countable.sort) Specif.sigT ->
Datatypes.natval unpickle_tagged :
Countable.coq_type ->
(Countable.sort -> Countable.coq_type) ->
Datatypes.nat ->
(Countable.sort, Countable.sort) Specif.sigT optionval coq_HB_unnamed_factory_118 :
Countable.coq_type ->
(Countable.sort -> Countable.coq_type) ->
(Countable.sort, Countable.sort) Specif.sigT Choice_isCountable.axioms_val coq_Specif_sigT__canonical__choice_Countable :
Countable.coq_type ->
(Countable.sort -> Countable.coq_type) ->
Countable.coq_typeval coq_HB_unnamed_factory_120 : Datatypes.nat Choice_isCountable.axioms_val coq_Datatypes_nat__canonical__choice_Countable : Countable.coq_typeval coq_HB_unnamed_factory_147 :
Countable.coq_type ->
Countable.sort option Countable.axioms_val coq_HB_unnamed_mixin_154 :
Countable.coq_type ->
Countable.sort option Choice_isCountable.axioms_val coq_Datatypes_option__canonical__choice_Countable :
Countable.coq_type ->
Countable.coq_typeval coq_HB_unnamed_factory_165 :
Countable.coq_type ->
Countable.coq_type ->
(Countable.sort * Countable.sort) Countable.axioms_val coq_HB_unnamed_mixin_172 :
Countable.coq_type ->
Countable.coq_type ->
(Countable.sort * Countable.sort) Choice_isCountable.axioms_val coq_Datatypes_prod__canonical__choice_Countable :
Countable.coq_type ->
Countable.coq_type ->
Countable.coq_typeval coq_HB_unnamed_factory_174 :
Countable.coq_type ->
Countable.coq_type ->
(Countable.sort, Countable.sort) Datatypes.sum Countable.axioms_val coq_HB_unnamed_mixin_181 :
Countable.coq_type ->
Countable.coq_type ->
(Countable.sort, Countable.sort) Datatypes.sum Choice_isCountable.axioms_val coq_Datatypes_sum__canonical__choice_Countable :
Countable.coq_type ->
Countable.coq_type ->
Countable.coq_type