package jasmin

  1. Overview
  2. Docs
package jasmin
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Jasmin.Choice

type __ = Obj.t
module CodeSeq : sig ... end
val seq_of_opt : 'a1 option -> 'a1 list
val tag_of_pair : ('a1 * 'a2) -> ('a1, 'a2) Specif.sigT
val pair_of_tag : ('a1, 'a2) Specif.sigT -> 'a1 * 'a2
val opair_of_sum : ('a1, 'a2) Datatypes.sum -> 'a1 option * 'a2 option
val sum_of_opair : ('a1 option * 'a2 option) -> ('a1, 'a2) Datatypes.sum option
module Coq_hasChoice : sig ... end
module Choice : sig ... end
val coq_PCanHasChoice : Choice.coq_type -> ('a1 -> Choice.sort) -> (Choice.sort -> 'a1 option) -> 'a1 Coq_hasChoice.phant_axioms
val coq_HB_unnamed_factory_6 : Choice.coq_type -> ('a1 -> Choice.sort) -> (Choice.sort -> 'a1 option) -> ('a1, Choice.sort) Eqtype.pcan_type Coq_hasChoice.phant_axioms
val eqtype_pcan_type__canonical__choice_Choice : Choice.coq_type -> ('a1 -> Choice.sort) -> (Choice.sort -> 'a1 option) -> Choice.coq_type
val coq_HB_unnamed_factory_9 : Choice.coq_type -> ('a1 -> Choice.sort) -> (Choice.sort -> 'a1) -> ('a1, Choice.sort) Eqtype.can_type Coq_hasChoice.phant_axioms
val eqtype_can_type__canonical__choice_Choice : Choice.coq_type -> ('a1 -> Choice.sort) -> (Choice.sort -> 'a1) -> Choice.coq_type
val coq_HB_unnamed_factory_16 : Choice.coq_type -> Choice.sort list Coq_hasChoice.phant_axioms
val coq_Datatypes_list__canonical__choice_Choice : Choice.coq_type -> Choice.coq_type
val coq_Specif_sigT__canonical__choice_Choice : Choice.coq_type -> (Choice.sort -> Choice.coq_type) -> Choice.coq_type
val coq_HB_unnamed_factory_20 : Datatypes.nat Coq_hasChoice.phant_axioms
val coq_Datatypes_nat__canonical__choice_Choice : Choice.coq_type
val 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_type
val coq_HB_unnamed_factory_50 : Choice.coq_type -> Choice.coq_type -> (Choice.sort * Choice.sort) Choice.axioms_
val coq_Datatypes_prod__canonical__choice_Choice : Choice.coq_type -> Choice.coq_type -> Choice.coq_type
module Choice_isCountable : sig ... end
module Countable : sig ... end
val unpickle : Countable.coq_type -> Datatypes.nat -> Countable.sort option
module Coq_isCountable : sig ... end
module Builders_77 : sig ... end
val 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_axioms
val 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_type
val coq_HB_unnamed_factory_93 : Countable.coq_type -> ('a1 -> Countable.sort) -> (Countable.sort -> 'a1) -> ('a1, Countable.sort) Eqtype.can_type Coq_isCountable.phant_axioms
val 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_type
val eqtype_sub_type__canonical__choice_Countable : Countable.coq_type -> Countable.sort Ssrbool.pred -> Countable.sort Eqtype.SubType.coq_type -> Countable.coq_type
val pickle_seq : Countable.coq_type -> Countable.sort list -> Datatypes.nat
val unpickle_seq : Countable.coq_type -> Datatypes.nat -> Countable.sort list option
val 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_type
val coq_Specif_sigT__canonical__choice_Countable : Countable.coq_type -> (Countable.sort -> Countable.coq_type) -> Countable.coq_type
val coq_HB_unnamed_factory_120 : Datatypes.nat Choice_isCountable.axioms_
val coq_Datatypes_nat__canonical__choice_Countable : Countable.coq_type
val 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_type
val coq_Datatypes_prod__canonical__choice_Countable : Countable.coq_type -> Countable.coq_type -> Countable.coq_type
val coq_Datatypes_sum__canonical__choice_Countable : Countable.coq_type -> Countable.coq_type -> Countable.coq_type