Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (26071 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1003 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (815 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1771 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (589 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (961 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (12021 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (508 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (308 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (479 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (496 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (906 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1204 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (4844 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (166 entries)

G

g [definition, in Stdlib.Logic.Berardi]
Gauss [lemma, in Stdlib.ZArith.Znumtheory]
Gcd [module, in Stdlib.Numbers.NatInt.NZGcd]
gcd [definition, in Stdlib.Init.Nat]
gcd [definition, in Stdlib.Numbers.Cyclic.Int63.Uint63]
gcd_spec [lemma, in Stdlib.Numbers.Cyclic.Int63.Uint63]
gcd_rec [definition, in Stdlib.Numbers.Cyclic.Int63.Uint63]
Gcd.gcd [axiom, in Stdlib.Numbers.NatInt.NZGcd]
ge [definition, in Stdlib.Init.Peano]
gen [lemma, in Stdlib.Init.Logic]
genCuttingPlane [definition, in Stdlib.micromega.ZMicromega]
genCuttingPlaneNone [lemma, in Stdlib.micromega.ZMicromega]
GeneralizedSetoidFunctionalChoice [abbreviation, in Stdlib.Logic.ChoiceFacts]
GeneralizedSetoidFunctionalChoice_on [definition, in Stdlib.Logic.ChoiceFacts]
generalized_excluded_middle [definition, in Stdlib.Logic.ClassicalFacts]
Generalized_induction_on_finite_sets [lemma, in Stdlib.Sets.Finite_sets_facts]
Generic [section, in Stdlib.Logic.Classical_Pred_Type]
Generic [module, in Stdlib.Logic.Hurkens]
GenericAbs [module, in Stdlib.Numbers.Integer.Abstract.ZSgnAbs]
GenericAbs.abs [definition, in Stdlib.Numbers.Integer.Abstract.ZSgnAbs]
GenericAbs.abs_neq [lemma, in Stdlib.Numbers.Integer.Abstract.ZSgnAbs]
GenericAbs.abs_eq [lemma, in Stdlib.Numbers.Integer.Abstract.ZSgnAbs]
GenericInstances [section, in Stdlib.Classes.Morphisms]
GenericInstances [section, in Stdlib.Classes.CMorphisms]
GenericInstances.A [variable, in Stdlib.Classes.Morphisms]
GenericInstances.B [variable, in Stdlib.Classes.Morphisms]
GenericInstances.C [variable, in Stdlib.Classes.Morphisms]
GenericInstances.U [variable, in Stdlib.Classes.Morphisms]
GenericMinMax [module, in Stdlib.Structures.GenericMinMax]
GenericMinMax [library]
GenericMinMax.ge_not_lt [lemma, in Stdlib.Structures.GenericMinMax]
GenericMinMax.max [definition, in Stdlib.Structures.GenericMinMax]
GenericMinMax.max_r [lemma, in Stdlib.Structures.GenericMinMax]
GenericMinMax.max_l [lemma, in Stdlib.Structures.GenericMinMax]
GenericMinMax.min [definition, in Stdlib.Structures.GenericMinMax]
GenericMinMax.min_r [lemma, in Stdlib.Structures.GenericMinMax]
GenericMinMax.min_l [lemma, in Stdlib.Structures.GenericMinMax]
GenericSgn [module, in Stdlib.Numbers.Integer.Abstract.ZSgnAbs]
GenericSgn.sgn [definition, in Stdlib.Numbers.Integer.Abstract.ZSgnAbs]
GenericSgn.sgn_neg [lemma, in Stdlib.Numbers.Integer.Abstract.ZSgnAbs]
GenericSgn.sgn_pos [lemma, in Stdlib.Numbers.Integer.Abstract.ZSgnAbs]
GenericSgn.sgn_null [lemma, in Stdlib.Numbers.Integer.Abstract.ZSgnAbs]
Generic.I [definition, in Stdlib.Logic.Hurkens]
Generic.induct [definition, in Stdlib.Logic.Hurkens]
Generic.le [definition, in Stdlib.Logic.Hurkens]
Generic.lemma1 [lemma, in Stdlib.Logic.Hurkens]
Generic.lemma2 [lemma, in Stdlib.Logic.Hurkens]
Generic.le' [definition, in Stdlib.Logic.Hurkens]
Generic.Omega [lemma, in Stdlib.Logic.Hurkens]
Generic.paradox [lemma, in Stdlib.Logic.Hurkens]
Generic.Paradox [section, in Stdlib.Logic.Hurkens]
Generic.Paradox.appU0 [variable, in Stdlib.Logic.Hurkens]
Generic.Paradox.appU1 [variable, in Stdlib.Logic.Hurkens]
Generic.Paradox.app0 [variable, in Stdlib.Logic.Hurkens]
Generic.Paradox.app1 [variable, in Stdlib.Logic.Hurkens]
Generic.Paradox.betaU1 [variable, in Stdlib.Logic.Hurkens]
Generic.Paradox.beta1 [variable, in Stdlib.Logic.Hurkens]
Generic.Paradox.El0 [variable, in Stdlib.Logic.Hurkens]
Generic.Paradox.El1 [variable, in Stdlib.Logic.Hurkens]
Generic.Paradox.F [variable, in Stdlib.Logic.Hurkens]
Generic.Paradox.ForallU0 [variable, in Stdlib.Logic.Hurkens]
Generic.Paradox.ForallU1 [variable, in Stdlib.Logic.Hurkens]
Generic.Paradox.Forall0 [variable, in Stdlib.Logic.Hurkens]
Generic.Paradox.Forall1 [variable, in Stdlib.Logic.Hurkens]
Generic.Paradox.lamU0 [variable, in Stdlib.Logic.Hurkens]
Generic.Paradox.lamU1 [variable, in Stdlib.Logic.Hurkens]
Generic.Paradox.lam0 [variable, in Stdlib.Logic.Hurkens]
Generic.Paradox.lam1 [variable, in Stdlib.Logic.Hurkens]
Generic.Paradox.u0 [variable, in Stdlib.Logic.Hurkens]
Generic.Paradox.U1 [variable, in Stdlib.Logic.Hurkens]
_ ·₀ [ _ ] [notation, in Stdlib.Logic.Hurkens]
_ ·₀ _ [notation, in Stdlib.Logic.Hurkens]
_ ⟶₀ _ [notation, in Stdlib.Logic.Hurkens]
_ ·₁ [ _ ] [notation, in Stdlib.Logic.Hurkens]
_ ·₁ _ [notation, in Stdlib.Logic.Hurkens]
_ ⟶₁ _ [notation, in Stdlib.Logic.Hurkens]
λ₀ _ , _ [notation, in Stdlib.Logic.Hurkens]
λ₀¹ _ , _ [notation, in Stdlib.Logic.Hurkens]
λ₁ _ , _ [notation, in Stdlib.Logic.Hurkens]
λ₂ _ , _ [notation, in Stdlib.Logic.Hurkens]
∀₀ _ : _ , _ [notation, in Stdlib.Logic.Hurkens]
∀₀¹ _ : _ , _ [notation, in Stdlib.Logic.Hurkens]
∀₁ _ : _ , _ [notation, in Stdlib.Logic.Hurkens]
∀₂ _ , _ [notation, in Stdlib.Logic.Hurkens]
Generic.sb [definition, in Stdlib.Logic.Hurkens]
Generic.U [variable, in Stdlib.Logic.Classical_Pred_Type]
Generic.U [definition, in Stdlib.Logic.Hurkens]
Generic.U0 [abbreviation, in Stdlib.Logic.Hurkens]
Generic.V [definition, in Stdlib.Logic.Hurkens]
Generic.WF [definition, in Stdlib.Logic.Hurkens]
gen_phiZ_morph [instance, in Stdlib.setoid_ring.Ncring_initial]
gen_phiZ_ext [lemma, in Stdlib.setoid_ring.Ncring_initial]
gen_phiZ_mul [lemma, in Stdlib.setoid_ring.Ncring_initial]
gen_phiZ_opp [lemma, in Stdlib.setoid_ring.Ncring_initial]
gen_phiZ_add [lemma, in Stdlib.setoid_ring.Ncring_initial]
gen_phiZ1_add_pos_neg [lemma, in Stdlib.setoid_ring.Ncring_initial]
gen_Zeqb_ok [lemma, in Stdlib.setoid_ring.Ncring_initial]
gen_phiZ [definition, in Stdlib.setoid_ring.Ncring_initial]
gen_phiZ1 [definition, in Stdlib.setoid_ring.Ncring_initial]
gen_phiPOS [definition, in Stdlib.setoid_ring.Ncring_initial]
gen_phiPOS1 [definition, in Stdlib.setoid_ring.Ncring_initial]
GEN_DIV.nphi [variable, in Stdlib.setoid_ring.InitialRing]
GEN_DIV.zphi [variable, in Stdlib.setoid_ring.InitialRing]
GEN_DIV.morph [variable, in Stdlib.setoid_ring.InitialRing]
GEN_DIV.ARth [variable, in Stdlib.setoid_ring.InitialRing]
GEN_DIV.Reqe [variable, in Stdlib.setoid_ring.InitialRing]
GEN_DIV.Rsth [variable, in Stdlib.setoid_ring.InitialRing]
GEN_DIV.phi [variable, in Stdlib.setoid_ring.InitialRing]
GEN_DIV.ceqb [variable, in Stdlib.setoid_ring.InitialRing]
GEN_DIV.copp [variable, in Stdlib.setoid_ring.InitialRing]
GEN_DIV.csub [variable, in Stdlib.setoid_ring.InitialRing]
GEN_DIV.cmul [variable, in Stdlib.setoid_ring.InitialRing]
GEN_DIV.cadd [variable, in Stdlib.setoid_ring.InitialRing]
GEN_DIV.cI [variable, in Stdlib.setoid_ring.InitialRing]
GEN_DIV.cO [variable, in Stdlib.setoid_ring.InitialRing]
GEN_DIV.C [variable, in Stdlib.setoid_ring.InitialRing]
GEN_DIV.req [variable, in Stdlib.setoid_ring.InitialRing]
GEN_DIV.ropp [variable, in Stdlib.setoid_ring.InitialRing]
GEN_DIV.rsub [variable, in Stdlib.setoid_ring.InitialRing]
GEN_DIV.rmul [variable, in Stdlib.setoid_ring.InitialRing]
GEN_DIV.radd [variable, in Stdlib.setoid_ring.InitialRing]
GEN_DIV.rI [variable, in Stdlib.setoid_ring.InitialRing]
GEN_DIV.rO [variable, in Stdlib.setoid_ring.InitialRing]
GEN_DIV.R [variable, in Stdlib.setoid_ring.InitialRing]
GEN_DIV [section, in Stdlib.setoid_ring.InitialRing]
gen_phiNword_morph [lemma, in Stdlib.setoid_ring.InitialRing]
gen_phiNword_ok [lemma, in Stdlib.setoid_ring.InitialRing]
gen_phiNword_Nwcons [lemma, in Stdlib.setoid_ring.InitialRing]
gen_phiNword_cons [lemma, in Stdlib.setoid_ring.InitialRing]
gen_phiNword0_ok [lemma, in Stdlib.setoid_ring.InitialRing]
gen_phiNword [definition, in Stdlib.setoid_ring.InitialRing]
gen_phiN_morph [lemma, in Stdlib.setoid_ring.InitialRing]
gen_phiN_sub [lemma, in Stdlib.setoid_ring.InitialRing]
gen_phiN_mult [lemma, in Stdlib.setoid_ring.InitialRing]
gen_phiN_add [lemma, in Stdlib.setoid_ring.InitialRing]
gen_phiN [definition, in Stdlib.setoid_ring.InitialRing]
gen_phiN1 [definition, in Stdlib.setoid_ring.InitialRing]
gen_phiZ_morph [lemma, in Stdlib.setoid_ring.InitialRing]
gen_phiZ_ext [lemma, in Stdlib.setoid_ring.InitialRing]
gen_phiZ_mul [lemma, in Stdlib.setoid_ring.InitialRing]
gen_phiZ_add [lemma, in Stdlib.setoid_ring.InitialRing]
gen_phiZ1_pos_sub [lemma, in Stdlib.setoid_ring.InitialRing]
gen_Zeqb_ok [lemma, in Stdlib.setoid_ring.InitialRing]
gen_phiZ [definition, in Stdlib.setoid_ring.InitialRing]
gen_phiZ1 [definition, in Stdlib.setoid_ring.InitialRing]
gen_phiPOS [definition, in Stdlib.setoid_ring.InitialRing]
gen_phiPOS1 [definition, in Stdlib.setoid_ring.InitialRing]
gen_setoid_fun_choice_imp_setoid_fun_choice [lemma, in Stdlib.Logic.ChoiceFacts]
gen_order_phi_Z [definition, in Stdlib.micromega.ZCoeff]
gen_phiZ_complete [lemma, in Stdlib.setoid_ring.Field_theory]
gen_phiZ_inj [lemma, in Stdlib.setoid_ring.Field_theory]
gen_phiPOS_discr_sgn [lemma, in Stdlib.setoid_ring.Field_theory]
gen_phiN_complete [lemma, in Stdlib.setoid_ring.Field_theory]
gen_phiN_inj [lemma, in Stdlib.setoid_ring.Field_theory]
gen_phiPOS_inj [lemma, in Stdlib.setoid_ring.Field_theory]
gen_st [definition, in Stdlib.Setoids.Setoid]
GeoCvZero [lemma, in Stdlib.Reals.Abstract.ConstructivePower]
GeoFiniteSum [lemma, in Stdlib.Reals.Abstract.ConstructivePower]
GeoHalfBelowTwo [lemma, in Stdlib.Reals.Abstract.ConstructivePower]
GeoHalfTwo [lemma, in Stdlib.Reals.Abstract.ConstructivePower]
get [definition, in Stdlib.rtauto.Bintree]
get [axiom, in Stdlib.Strings.PrimString]
get [definition, in Stdlib.Strings.String]
get [axiom, in Stdlib.Array.PArray]
get_map [lemma, in Stdlib.rtauto.Bintree]
get_In [lemma, in Stdlib.rtauto.Bintree]
get_push_Full [lemma, in Stdlib.rtauto.Bintree]
get_Full_Eq [lemma, in Stdlib.rtauto.Bintree]
get_Full_Gt [lemma, in Stdlib.rtauto.Bintree]
get_empty [lemma, in Stdlib.rtauto.Bintree]
get_signZ [definition, in Stdlib.setoid_ring.Ncring_initial]
get_char63_valid [lemma, in Stdlib.Strings.PString]
get_spec_not_in_bounds [lemma, in Stdlib.Strings.PString]
get_spec_in_bounds [lemma, in Stdlib.Strings.PString]
get_spec [axiom, in Stdlib.Strings.PrimStringAxioms]
get_signZ_th [lemma, in Stdlib.setoid_ring.InitialRing]
get_signZ [definition, in Stdlib.setoid_ring.InitialRing]
get_PEopp [definition, in Stdlib.micromega.EnvRing]
get_sign [definition, in Stdlib.Floats.PrimFloat]
get_correct [lemma, in Stdlib.Strings.String]
get_not_default_lt [lemma, in Stdlib.Array.PArray]
get_set_same_default [lemma, in Stdlib.Array.PArray]
get_copy [axiom, in Stdlib.Array.PArray]
get_make [axiom, in Stdlib.Array.PArray]
get_set_other [axiom, in Stdlib.Array.PArray]
get_set_same [axiom, in Stdlib.Array.PArray]
get_out_of_bounds [axiom, in Stdlib.Array.PArray]
get_PEopp [definition, in Stdlib.setoid_ring.Ring_polynom]
get_sign_None_th [lemma, in Stdlib.setoid_ring.Ring_theory]
get_sign_None [definition, in Stdlib.setoid_ring.Ring_theory]
get_digit [definition, in Stdlib.Numbers.Cyclic.Int63.Uint63]
ge_bool_cases [lemma, in Stdlib.micromega.RingMicromega]
ge_bool [definition, in Stdlib.micromega.RingMicromega]
ge_dec [lemma, in Stdlib.Arith.Compare_dec]
GFormula [inductive, in Stdlib.micromega.Tauto]
GFormula_sind [definition, in Stdlib.micromega.Tauto]
GFormula_rec [definition, in Stdlib.micromega.Tauto]
GFormula_ind [definition, in Stdlib.micromega.Tauto]
GFormula_rect [definition, in Stdlib.micromega.Tauto]
Glb [inductive, in Stdlib.Sets.Cpo]
glb [definition, in Stdlib.Reals.SeqProp]
glb_dec_Q [lemma, in Stdlib.Reals.Abstract.ConstructiveLUB]
Glb_sind [definition, in Stdlib.Sets.Cpo]
Glb_rec [definition, in Stdlib.Sets.Cpo]
Glb_ind [definition, in Stdlib.Sets.Cpo]
Glb_rect [definition, in Stdlib.Sets.Cpo]
Glb_definition [constructor, in Stdlib.Sets.Cpo]
gmax [definition, in Stdlib.Structures.GenericMinMax]
gmin [definition, in Stdlib.Structures.GenericMinMax]
GodelDummett [definition, in Stdlib.Logic.ClassicalFacts]
Godel_Dummett_weak_excluded_middle [lemma, in Stdlib.Logic.ClassicalFacts]
Godel_Dummett_iff_right_distr_implication_over_disjunction [lemma, in Stdlib.Logic.ClassicalFacts]
GP_infinite [lemma, in Stdlib.Reals.Rseries]
GP_finite [lemma, in Stdlib.Reals.Rfunctions]
growing_ineq [lemma, in Stdlib.Reals.Abstract.ConstructiveLimits]
growing_prop [lemma, in Stdlib.Reals.Rseries]
growing_ineq [lemma, in Stdlib.Reals.SeqProp]
growing_cv [lemma, in Stdlib.Reals.SeqProp]
Gt [constructor, in Stdlib.Init.Datatypes]
GT [record, in Stdlib.micromega.DeclConstant]
GT [constructor, in Stdlib.Structures.OrderedType]
gt [definition, in Stdlib.Init.Peano]
gtof [definition, in Stdlib.Arith.Wf_nat]
Gt_Psucc [lemma, in Stdlib.rtauto.Bintree]
GT_APP2 [instance, in Stdlib.micromega.DeclConstant]
GT_APP1 [instance, in Stdlib.micromega.DeclConstant]
GT_O [instance, in Stdlib.micromega.DeclConstant]
gt_wf_ind [lemma, in Stdlib.Arith.Wf_nat]
gt_wf_rec [lemma, in Stdlib.Arith.Wf_nat]
gt_wf_rect [lemma, in Stdlib.Arith.Wf_nat]
gt_le_trans_stt [definition, in Stdlib.Arith.Arith_base]
gt_trans_S_stt [definition, in Stdlib.Arith.Arith_base]
gt_le_S_stt [definition, in Stdlib.Arith.Arith_base]
gt_S_le_stt [definition, in Stdlib.Arith.Arith_base]
gt_not_le_stt [definition, in Stdlib.Arith.Arith_base]
gt_asym_stt [definition, in Stdlib.Arith.Arith_base]
gt_irrefl_stt [definition, in Stdlib.Arith.Arith_base]
gt_pred_stt [definition, in Stdlib.Arith.Arith_base]
gt_S_n_stt [definition, in Stdlib.Arith.Arith_base]
gt_n_S_stt [definition, in Stdlib.Arith.Arith_base]
gt_Sn_n_stt [definition, in Stdlib.Arith.Arith_base]
gt_Sn_O_stt [definition, in Stdlib.Arith.Arith_base]
gt_dec [lemma, in Stdlib.Arith.Compare_dec]
gt_eq_gt_dec [definition, in Stdlib.Arith.Compare_dec]
GuardedFunctionalChoice [abbreviation, in Stdlib.Logic.ChoiceFacts]
GuardedFunctionalChoice_on [definition, in Stdlib.Logic.ChoiceFacts]
GuardedFunctionalRelReification [abbreviation, in Stdlib.Logic.ChoiceFacts]
GuardedFunctionalRelReification_on [definition, in Stdlib.Logic.ChoiceFacts]
GuardedRelationalChoice [abbreviation, in Stdlib.Logic.ChoiceFacts]
GuardedRelationalChoice_on [definition, in Stdlib.Logic.ChoiceFacts]
guarded_iff_omniscient_fun_choice [lemma, in Stdlib.Logic.ChoiceFacts]
guarded_fun_choice_imp_fun_choice [lemma, in Stdlib.Logic.ChoiceFacts]
guarded_fun_choice_imp_indep_of_general_premises [lemma, in Stdlib.Logic.ChoiceFacts]
guarded_iff_omniscient_rel_choice [lemma, in Stdlib.Logic.ChoiceFacts]
guarded_rel_choice_imp_rel_choice [lemma, in Stdlib.Logic.ChoiceFacts]
guarded_rel_choice [lemma, in Stdlib.Logic.Diaconescu]
g_adjoint [definition, in Stdlib.Logic.Adjointification]


Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (26071 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1003 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (815 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1771 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (589 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (961 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (12021 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (508 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (308 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (479 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (496 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (906 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1204 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (4844 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (166 entries)