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/Eqtype/index.html
Module Jasmin.Eqtype
type __ = Obj.ttype 't eq_axiom = 't -> 't -> Bool.reflectmodule Coq_hasDecEq : sig ... endmodule Equality : sig ... endval eq_op : Equality.coq_type -> Equality.sort Ssrbool.relval eqP : Equality.coq_type -> Equality.sort eq_axiomval unit_eqP : unit eq_axiomval coq_HB_unnamed_factory_1 : unit Coq_hasDecEq.axioms_val coq_Datatypes_unit__canonical__eqtype_Equality : Equality.coq_typeval eqbP : bool eq_axiomval coq_HB_unnamed_factory_3 : bool Coq_hasDecEq.axioms_val coq_Datatypes_bool__canonical__eqtype_Equality : Equality.coq_typeval pred1 :
Equality.coq_type ->
Equality.sort ->
Equality.sort Ssrbool.simpl_predmodule Coq_isSub : sig ... endmodule SubType : sig ... endval coq_Sub :
'a1 Ssrbool.pred ->
'a1 SubType.coq_type ->
'a1 ->
'a1 SubType.sortval insub :
'a1 Ssrbool.pred ->
'a1 SubType.coq_type ->
'a1 ->
'a1 SubType.sort optionval inj_eqAxiom : Equality.coq_type -> ('a1 -> Equality.sort) -> 'a1 eq_axiomval 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_typeval 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 pair_eq :
Equality.coq_type ->
Equality.coq_type ->
(Equality.sort * Equality.sort) Ssrbool.relval pair_eqP :
Equality.coq_type ->
Equality.coq_type ->
(Equality.sort * Equality.sort) eq_axiomval coq_HB_unnamed_factory_38 :
Equality.coq_type ->
Equality.coq_type ->
(Equality.sort * Equality.sort) Coq_hasDecEq.axioms_val coq_Datatypes_prod__canonical__eqtype_Equality :
Equality.coq_type ->
Equality.coq_type ->
Equality.coq_typeval opt_eq :
Equality.coq_type ->
Equality.sort option ->
Equality.sort option ->
boolval opt_eqP : Equality.coq_type -> Equality.sort option eq_axiomval 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_typeval tagged_as :
Equality.coq_type ->
(Equality.sort, 'a1) Specif.sigT ->
(Equality.sort, 'a1) Specif.sigT ->
'a1val tag_eq :
Equality.coq_type ->
(Equality.sort -> Equality.coq_type) ->
(Equality.sort, Equality.sort) Specif.sigT ->
(Equality.sort, Equality.sort) Specif.sigT ->
boolval tag_eqP :
Equality.coq_type ->
(Equality.sort -> Equality.coq_type) ->
(Equality.sort, Equality.sort) Specif.sigT eq_axiomval coq_HB_unnamed_factory_42 :
Equality.coq_type ->
(Equality.sort -> Equality.coq_type) ->
(Equality.sort, Equality.sort) Specif.sigT Coq_hasDecEq.axioms_val sum_eq :
Equality.coq_type ->
Equality.coq_type ->
(Equality.sort, Equality.sort) Datatypes.sum ->
(Equality.sort, Equality.sort) Datatypes.sum ->
boolval sum_eqP :
Equality.coq_type ->
Equality.coq_type ->
(Equality.sort, Equality.sort) Datatypes.sum eq_axiomval coq_HB_unnamed_factory_44 :
Equality.coq_type ->
Equality.coq_type ->
(Equality.sort, Equality.sort) Datatypes.sum Coq_hasDecEq.axioms_