package jasmin

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

Module Jasmin.Eqtype

type __ = Obj.t
type 't eq_axiom = 't -> 't -> Bool.reflect
module Coq_hasDecEq : sig ... end
module Equality : sig ... end
val unit_eqP : unit eq_axiom
val coq_HB_unnamed_factory_1 : unit Coq_hasDecEq.axioms_
val coq_Datatypes_unit__canonical__eqtype_Equality : Equality.coq_type
val eqb : bool -> bool -> bool
val eqbP : bool eq_axiom
val coq_HB_unnamed_factory_3 : bool Coq_hasDecEq.axioms_
val coq_Datatypes_bool__canonical__eqtype_Equality : Equality.coq_type
module Coq_isSub : sig ... end
module SubType : sig ... end
val coq_Sub : 'a1 Ssrbool.pred -> 'a1 SubType.coq_type -> 'a1 -> 'a1 SubType.sort
val insub : 'a1 Ssrbool.pred -> 'a1 SubType.coq_type -> 'a1 -> 'a1 SubType.sort option
type ('t, 'x) inj_type = 't
type ('t, 'x) pcan_type = 't
type ('t, 'x) can_type = 't
val inj_eqAxiom : Equality.coq_type -> ('a1 -> Equality.sort) -> 'a1 eq_axiom
val coq_HB_unnamed_factory_9 : Equality.coq_type -> ('a1 -> Equality.sort) -> ('a1, Equality.sort) inj_type Coq_hasDecEq.axioms_
val eqtype_inj_type__canonical__eqtype_Equality : Equality.coq_type -> ('a1 -> Equality.sort) -> Equality.coq_type
val coq_HB_unnamed_factory_12 : Equality.coq_type -> ('a1 -> Equality.sort) -> (Equality.sort -> 'a1 option) -> ('a1, Equality.sort) pcan_type Equality.axioms_
val coq_HB_unnamed_mixin_14 : Equality.coq_type -> ('a1 -> Equality.sort) -> (Equality.sort -> 'a1 option) -> ('a1, Equality.sort) pcan_type Coq_hasDecEq.axioms_
val coq_HB_unnamed_factory_16 : Equality.coq_type -> ('a1 -> Equality.sort) -> (Equality.sort -> 'a1) -> ('a1, Equality.sort) can_type Equality.axioms_
val coq_HB_unnamed_mixin_19 : Equality.coq_type -> ('a1 -> Equality.sort) -> (Equality.sort -> 'a1) -> ('a1, Equality.sort) can_type Coq_hasDecEq.axioms_
val coq_Datatypes_prod__canonical__eqtype_Equality : Equality.coq_type -> Equality.coq_type -> Equality.coq_type
val opt_eq : Equality.coq_type -> Equality.sort option -> Equality.sort option -> bool
val opt_eqP : Equality.coq_type -> Equality.sort option eq_axiom
val coq_HB_unnamed_factory_40 : Equality.coq_type -> Equality.sort option Coq_hasDecEq.axioms_
val coq_Datatypes_option__canonical__eqtype_Equality : Equality.coq_type -> Equality.coq_type
val tagged_as : Equality.coq_type -> (Equality.sort, 'a1) Specif.sigT -> (Equality.sort, 'a1) Specif.sigT -> 'a1