H
HasAbs [module, in HasAbs]
HasAbs.abs [axiom, in abs]
HasAbs.abs_eq [axiom, in abs_eq]
HasAbs.abs_neq [axiom, in abs_neq]
HasBoolOrdFuns [module, in HasBoolOrdFuns]
HasBoolOrdFuns' [module, in HasBoolOrdFuns']
HasCmp [module, in HasCmp]
HasCmp.compare [axiom, in compare]
HasCompare [module, in HasCompare]
HasEq [module, in HasEq]
HasEqb [module, in HasEqb]
HasEqBool [module, in HasEqBool]
HasEqBool2Dec [module, in HasEqBool2Dec]
HasEqBool2Dec.eq_dec [lemma, in eq_dec]
HasEqb.eqb [axiom, in eqb]
HasEqDec [module, in HasEqDec]
HasEqDec.eq_dec [axiom, in eq_dec]
HasEqDec2Bool [module, in HasEqDec2Bool]
HasEqDec2Bool.eqb [definition, in eqb]
HasEqDec2Bool.eqb_eq [lemma, in eqb_eq]
HasEq.eq [axiom, in eq]
HasLe [module, in HasLe]
HasLeb [module, in HasLeb]
HasLeb.leb [axiom, in leb]
HasLe.le [axiom, in le]
HasLt [module, in HasLt]
HasLtb [module, in HasLtb]
HasLtb.ltb [axiom, in ltb]
HasLt.lt [axiom, in lt]
HasMax [module, in HasMax]
HasMax.max [axiom, in max]
HasMax.max_r [axiom, in max_r]
HasMax.max_l [axiom, in max_l]
HasMin [module, in HasMin]
HasMinMax [module, in HasMinMax]
HasMin.min [axiom, in min]
HasMin.min_r [axiom, in min_r]
HasMin.min_l [axiom, in min_l]
HasOrdOps [module, in HasOrdOps]
HasOrdOps.compare [axiom, in compare]
HasOrdOps.max_elt [axiom, in max_elt]
HasOrdOps.min_elt [axiom, in min_elt]
HasSgn [module, in HasSgn]
HasSgn.sgn [axiom, in sgn]
HasSgn.sgn_pos [axiom, in sgn_pos]
HasSgn.sgn_null [axiom, in sgn_null]
HasSgn.sgn_neg [axiom, in sgn_neg]
HasUsualEq [module, in HasUsualEq]
HasUsualEq.eq [definition, in eq]
HasWOps [module, in HasWOps]
HasWOps.add [axiom, in add]
HasWOps.cardinal [axiom, in cardinal]
HasWOps.choose [axiom, in choose]
HasWOps.diff [axiom, in diff]
HasWOps.elements [axiom, in elements]
HasWOps.empty [axiom, in empty]
HasWOps.equal [axiom, in equal]
HasWOps.exists_ [axiom, in exists_]
HasWOps.filter [axiom, in filter]
HasWOps.fold [axiom, in fold]
HasWOps.for_all [axiom, in for_all]
HasWOps.inter [axiom, in inter]
HasWOps.is_empty [axiom, in is_empty]
HasWOps.mem [axiom, in mem]
HasWOps.partition [axiom, in partition]
HasWOps.remove [axiom, in remove]
HasWOps.singleton [axiom, in singleton]
HasWOps.subset [axiom, in subset]
HasWOps.union [axiom, in union]
has_lb [definition, in has_lb]
has_ub [definition, in has_ub]
has_unique_least_element [definition, in has_unique_least_element]
has_fixpoint [record, in has_fixpoint]
hd [definition, in hd]
hd [definition, in hd]
hd [definition, in hd]
HdRel [inductive, in HdRel]
HdRel_nil [constructor, in HdRel_nil]
HdRel_cons [constructor, in HdRel_cons]
HdRel_inv [lemma, in HdRel_inv]
hd_error [definition, in hd_error]
hd_error_cons [lemma, in hd_error_cons]
hd_error_nil [lemma, in hd_error_nil]
head [abbreviation, in head]
head_cons [abbreviation, in head_cons]
head_nil [abbreviation, in head_nil]
head0 [definition, in head0]
head031 [definition, in head031]
head031_equiv [lemma, in head031_equiv]
head031_alt [definition, in head031_alt]
Heap [library]
heap_exist [constructor, in heap_exist]
heap_to_list [lemma, in heap_to_list]
Heine [lemma, in Heine]
Heine_cor2 [lemma, in Heine_cor2]
Heine_cor1 [lemma, in Heine_cor1]
HelloWorld [definition, in HelloWorld]
Here [constructor, in Here]
HereAndFurther [constructor, in HereAndFurther]
high [definition, in high]
Homomorphism [module, in Homomorphism]
Homomorphism.homomorphism [definition, in homomorphism]
Homomorphism.hom_nat_iso [lemma, in hom_nat_iso]
Homomorphism.natural_isomorphism_0 [lemma, in natural_isomorphism_0]
Homomorphism.natural_isomorphism [definition, in natural_isomorphism]
Homomorphism.natural_isomorphism_succ [lemma, in natural_isomorphism_succ]
Homomorphism.natural_isomorphism_wd [instance, in natural_isomorphism_wd]
_ == _ [notation, in ::x_'=='_x]
Hurkens [library]