Choice (p.jasmin.2026.03.1.doc.jasmin.jasmin.Jasmin.Choice)

type __ = Obj.t

module Coq_hasChoice : sig ... end

module Choice : sig ... end

val find_subdef : 
  Choice.coq_type ->
  Choice.sort Ssrbool.pred ->
  Datatypes.nat ->
  Choice.sort option

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 nat_hasChoice : Datatypes.nat Coq_hasChoice.phant_axioms

val coq_HB_unnamed_factory_20 : Datatypes.nat Coq_hasChoice.phant_axioms

val coq_Datatypes_nat__canonical__choice_Choice : Choice.coq_type

module Choice_isCountable : sig ... end

module Countable : sig ... end

val pickle : Countable.coq_type -> Countable.sort -> Datatypes.nat

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_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_mixin_106 : 
  Countable.coq_type ->
  Countable.sort Ssrbool.pred ->
  Countable.sort Eqtype.SubType.coq_type ->
  Choice.sort Eqtype.SubType.sort Coq_hasChoice.phant_axioms

val 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_type

val coq_HB_unnamed_factory_120 : Datatypes.nat Choice_isCountable.axioms_

val coq_Datatypes_nat__canonical__choice_Countable : Countable.coq_type