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

(19204 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

(228 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

(298 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

(1273 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

(313 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

(8163 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

(1514 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

(52 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

(352 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

(534 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

(727 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

(402 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

(333 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

(4833 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

(182 entries)

---

I

iBox [definition, in MetaRocq.Erasure.EImplementBox]
idecl_binder [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
ident [definition, in MetaRocq.Common.Kernames]
identity_typing [lemma, in MetaRocq.Examples.typing_correctness]
IdentMap [module, in MetaRocq.Common.Kernames]
IdentMapDecide [module, in MetaRocq.Common.Kernames]
IdentMapExtraFact [module, in MetaRocq.Common.Kernames]
IdentMapFact [module, in MetaRocq.Common.Kernames]
IdentOT [module, in MetaRocq.Common.Kernames]
IdentOTOrig [module, in MetaRocq.Common.Kernames]
IdentSet [module, in MetaRocq.Common.Kernames]
IdentSetDecide [module, in MetaRocq.Common.Kernames]
IdentSetExtraDecide [module, in MetaRocq.Common.Kernames]
IdentSetExtraOrdProp [module, in MetaRocq.Common.Kernames]
IdentSetFact [module, in MetaRocq.Common.Kernames]
IdentSetOrdProp [module, in MetaRocq.Common.Kernames]
IdentSetProp [module, in MetaRocq.Common.Kernames]
ident_of_name [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
ids [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
idsn [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
idsn_spec [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
idsn_lt [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
idsn_length [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
id_nth_spec [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
id_monad [instance, in MetaRocq.Utils.monad_utils]
id_id [lemma, in MetaRocq.PCUIC.PCUICAst]
id_nat [definition, in MetaRocq.Examples.demo]
id_proper_proxy [instance, in MetaRocq.Utils.MRPrelude]
iffT_l [definition, in MetaRocq.Utils.MRRelations]
iff_is_true_eq_bool [lemma, in MetaRocq.Utils.MRUtils]
iff_ex [lemma, in MetaRocq.Utils.MRUtils]
iff_forall [lemma, in MetaRocq.Utils.MRUtils]
iff_reflect [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
if_true_false [lemma, in MetaRocq.Utils.MRUtils]
IHup [lemma, in MetaRocq.PCUIC.PCUICInductives]
IllFormedDecl [constructor, in MetaRocq.SafeChecker.PCUICErrors]
IllFormedDecl [constructor, in MetaRocq.Template.Checker]
IllFormedFix [constructor, in MetaRocq.SafeChecker.PCUICErrors]
IllFormedFix [constructor, in MetaRocq.Template.Checker]
Imp [constructor, in MetaRocq.Examples.tauto]
impl [definition, in MetaRocq.Common.config]
implement_box_eval [lemma, in MetaRocq.Erasure.EImplementBox]
implement_box_mkApps [lemma, in MetaRocq.Erasure.EImplementBox]
implement_box_env_extends [lemma, in MetaRocq.Erasure.EImplementBox]
implement_box_env_wf_glob [lemma, in MetaRocq.Erasure.EImplementBox]
implement_box_declared_constant [lemma, in MetaRocq.Erasure.EImplementBox]
implement_box_isLazyApp [lemma, in MetaRocq.Erasure.EImplementBox]
implement_box_isPrimApp [lemma, in MetaRocq.Erasure.EImplementBox]
implement_box_isConstructApp [lemma, in MetaRocq.Erasure.EImplementBox]
implement_box_program [definition, in MetaRocq.Erasure.EImplementBox]
implement_box_env [definition, in MetaRocq.Erasure.EImplementBox]
implement_box_decl [definition, in MetaRocq.Erasure.EImplementBox]
implement_box_constant_decl [definition, in MetaRocq.Erasure.EImplementBox]
implement_box_nth [lemma, in MetaRocq.Erasure.EImplementBox]
implement_box_cunfold_cofix [lemma, in MetaRocq.Erasure.EImplementBox]
implement_box_cunfold_fix [lemma, in MetaRocq.Erasure.EImplementBox]
implement_box_cofix_subst [lemma, in MetaRocq.Erasure.EImplementBox]
implement_box_fix_subst [lemma, in MetaRocq.Erasure.EImplementBox]
implement_box_iota_red [lemma, in MetaRocq.Erasure.EImplementBox]
implement_box_substl [lemma, in MetaRocq.Erasure.EImplementBox]
implement_box_csubst [lemma, in MetaRocq.Erasure.EImplementBox]
implement_box_lift [lemma, in MetaRocq.Erasure.EImplementBox]
implement_box [definition, in MetaRocq.Erasure.EImplementBox]
implement_box.Def [section, in MetaRocq.Erasure.EImplementBox]
implement_box.Σ [variable, in MetaRocq.Erasure.EImplementBox]
implement_box [section, in MetaRocq.Erasure.EImplementBox]
implP_Proper [instance, in MetaRocq.Utils.MRPred]
implP_Proper [instance, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
impl_ctrans [definition, in MetaRocq.Common.config]
impl_trans [definition, in MetaRocq.Common.config]
impl_crefl [definition, in MetaRocq.Common.config]
impl_refl [definition, in MetaRocq.Common.config]
impl_reflb [definition, in MetaRocq.Common.config]
ImportDefaultBehavior [constructor, in MetaRocq.Template.TemplateMonad.Common]
ImportNeedQualified [constructor, in MetaRocq.Template.TemplateMonad.Common]
import_status [inductive, in MetaRocq.Template.TemplateMonad.Common]
impredicative_product [lemma, in MetaRocq.Common.Universes]
impredicative_csort_product [lemma, in MetaRocq.Common.Universes]
inat [abbreviation, in MetaRocq.Examples.demo]
InA_In_eq [lemma, in MetaRocq.Utils.MRList]
includes_deps_fold [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
includes_deps_union [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
includes_deps [definition, in MetaRocq.Erasure.ErasureFunctionProperties]
includes_deps_equiv [lemma, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
include_supermodule_of_submodule_inclusion [definition, in MetaRocq.Quotation.ToPCUIC.Init]
include_submodule_of_submodule_inclusion [definition, in MetaRocq.Quotation.ToPCUIC.Init]
include_supermodule_of_submodule_inclusion [definition, in MetaRocq.Quotation.ToTemplate.Init]
include_submodule_of_submodule_inclusion [definition, in MetaRocq.Quotation.ToTemplate.Init]
incl_cs_trans [lemma, in MetaRocq.Common.Universes]
incl_cs_refl [lemma, in MetaRocq.Common.Universes]
incl_cs_refl [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
incl_cs_refl [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
inddecl_name [definition, in MetaRocq.PCUIC.PCUICCasesHelper]
IndFix [constructor, in MetaRocq.SafeChecker.PCUICSafeConversion]
indices_matter [projection, in MetaRocq.Common.config]
indpred_ctx [definition, in MetaRocq.PCUIC.PCUICCasesHelper]
IndRef [constructor, in MetaRocq.Common.Kernames]
inds [definition, in MetaRocq.PCUIC.PCUICAst]
inds [definition, in MetaRocq.Template.Ast]
inds_nth_error [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
inds_is_open_terms [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
inds_nth_error [lemma, in MetaRocq.Erasure.EArities]
inds_spec [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
inds_length [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
inds_spec [lemma, in MetaRocq.Template.Ast]
inds_length [lemma, in MetaRocq.Template.Ast]
Induction [library]
inductive [record, in MetaRocq.Common.Kernames]
InductiveDecl [constructor, in MetaRocq.Erasure.Typed.ExAst]
InductiveDecl [constructor, in MetaRocq.Erasure.EAst]
inductives_mapping [definition, in MetaRocq.Erasure.EProgram]
inductive_cumulative_indices_smash [lemma, in MetaRocq.SafeChecker.PCUICSafeRetyping]
inductive_quotation_of [record, in MetaRocq.Quotation.ToPCUIC.Init]
inductive_cumulative_indices [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
inductive_mapping [definition, in MetaRocq.Erasure.EProgram]
inductive_quotation_of [record, in MetaRocq.Quotation.ToTemplate.Init]
inductive_ind_ind_bodies_length [lemma, in MetaRocq.PCUIC.PCUICInductives]
inductive_ind [projection, in MetaRocq.Common.Kernames]
inductive_mind [projection, in MetaRocq.Common.Kernames]
inductive_arity [definition, in MetaRocq.Erasure.Extract]
inductive_isprop_and_pars_trans_env_debox_types [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
inductive_isprop_and_pars_trans_env_dearg_env [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
inductive_isprop_and_pars [definition, in MetaRocq.Erasure.EGlobalEnv]
ind_aname [definition, in MetaRocq.Erasure.Typed.Erasure]
ind_cons [constructor, in MetaRocq.PCUIC.Bidirectional.BDTyping]
ind_bodies [projection, in MetaRocq.Erasure.Typed.ExAst]
ind_npars [projection, in MetaRocq.Erasure.Typed.ExAst]
ind_finite [projection, in MetaRocq.Erasure.Typed.ExAst]
ind_projs [projection, in MetaRocq.Erasure.Typed.ExAst]
ind_ctors [projection, in MetaRocq.Erasure.Typed.ExAst]
ind_type_vars [projection, in MetaRocq.Erasure.Typed.ExAst]
ind_kelim [projection, in MetaRocq.Erasure.Typed.ExAst]
ind_propositional [projection, in MetaRocq.Erasure.Typed.ExAst]
ind_name [projection, in MetaRocq.Erasure.Typed.ExAst]
ind_masks [projection, in MetaRocq.Erasure.Typed.Optimize]
ind_info_nmind [projection, in MetaRocq.Erasure.Typed.CertifyingEta]
ind_info_inductive [projection, in MetaRocq.Erasure.Typed.CertifyingEta]
ind_info [record, in MetaRocq.Erasure.Typed.CertifyingEta]
ind_binder [definition, in MetaRocq.PCUIC.PCUICCasesContexts]
ind_projs_reorder [lemma, in MetaRocq.Erasure.EReorderCstrs]
ind_ctors_no_reorder [lemma, in MetaRocq.Erasure.EReorderCstrs]
ind_ctors_reorder [lemma, in MetaRocq.Erasure.EReorderCstrs]
ind_bodies [projection, in MetaRocq.Erasure.EAst]
ind_npars [projection, in MetaRocq.Erasure.EAst]
ind_finite [projection, in MetaRocq.Erasure.EAst]
ind_projs [projection, in MetaRocq.Erasure.EAst]
ind_ctors [projection, in MetaRocq.Erasure.EAst]
ind_kelim [projection, in MetaRocq.Erasure.EAst]
ind_propositional [projection, in MetaRocq.Erasure.EAst]
ind_name [projection, in MetaRocq.Erasure.EAst]
ind_whnf_classification [lemma, in MetaRocq.PCUIC.PCUICClassification]
ind_whnf_classification' [lemma, in MetaRocq.PCUIC.PCUICClassification]
ind_predicate_context_length [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
ind_predicate_context [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
ind_subst [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
ind_predicate_context_length [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
ind_predicate_context [definition, in MetaRocq.Template.Ast]
infer [definition, in MetaRocq.SafeChecker.PCUICSafeRetyping]
infer [definition, in MetaRocq.Template.Checker]
infer [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
infering [inductive, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_prod_on_free_vars [lemma, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
infering_on_free_vars [lemma, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
infering_indu_size_pos [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_prod_size_pos [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_sort_size_pos [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_size_pos [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_indu_size [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_prod_size [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_sort_size [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_size [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_indu_sind [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_indu_rec [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_indu_ind [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_indu_rect [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_prod_sind [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_prod_rec [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_prod_ind [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_prod_rect [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_sort_sind [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_sort_rec [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_sort_ind [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_sort_rect [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_sind [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_rec [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_ind [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_rect [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_indu [inductive, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_prod [inductive, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_sort [inductive, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_ind_infering [lemma, in MetaRocq.PCUIC.Bidirectional.BDUnique]
infering_ind_ind' [lemma, in MetaRocq.PCUIC.Bidirectional.BDUnique]
infering_ind_ind [lemma, in MetaRocq.PCUIC.Bidirectional.BDUnique]
infering_prod_infering [lemma, in MetaRocq.PCUIC.Bidirectional.BDUnique]
infering_prod_prod' [lemma, in MetaRocq.PCUIC.Bidirectional.BDUnique]
infering_prod_prod [lemma, in MetaRocq.PCUIC.Bidirectional.BDUnique]
infering_sort_infering [lemma, in MetaRocq.PCUIC.Bidirectional.BDUnique]
infering_sort_sort [lemma, in MetaRocq.PCUIC.Bidirectional.BDUnique]
infering_checking [lemma, in MetaRocq.PCUIC.Bidirectional.BDUnique]
infering_unique' [lemma, in MetaRocq.PCUIC.Bidirectional.BDUnique]
infering_unique [lemma, in MetaRocq.PCUIC.Bidirectional.BDUnique]
infering_ind_typing [lemma, in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
infering_prod_typing [lemma, in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
infering_sort_isType [lemma, in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
infering_sort_typing [lemma, in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
infering_typing [lemma, in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
infer_ind_Ind [constructor, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infer_prod_Prod [constructor, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infer_sort_Sort [constructor, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infer_Prim [constructor, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infer_CoFix [constructor, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infer_Fix [constructor, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infer_Proj [constructor, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infer_Case [constructor, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infer_Construct [constructor, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infer_Ind [constructor, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infer_Const [constructor, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infer_App [constructor, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infer_LetIn [constructor, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infer_Lambda [constructor, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infer_Prod [constructor, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infer_Sort [constructor, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infer_Rel [constructor, in MetaRocq.PCUIC.Bidirectional.BDTyping]
infer_and_print_template_program_with_guard [definition, in MetaRocq.SafeCheckerPlugin.Extraction]
infer_as_prod [definition, in MetaRocq.SafeChecker.PCUICSafeRetyping]
infer_as_sort [definition, in MetaRocq.SafeChecker.PCUICSafeRetyping]
infer_replacement_inductive [definition, in MetaRocq.Quotation.ToPCUIC.Init]
infer_irrel [lemma, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
infer_as_sort_irrel [lemma, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
infer_as_prod_irrel [lemma, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
infer_irrel.hl [variable, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
infer_irrel.normalization_in' [variable, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
infer_irrel.normalization_in [variable, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
infer_irrel.X' [variable, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
infer_irrel.X_type' [variable, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
infer_irrel.X [variable, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
infer_irrel.X_type [variable, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
infer_irrel.nor [variable, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
infer_irrel.cf [variable, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
infer_irrel [section, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
infer_and_print_template_program [definition, in MetaRocq.SafeCheckerPlugin.SafeTemplateChecker]
infer_template_program [definition, in MetaRocq.SafeCheckerPlugin.SafeTemplateChecker]
infer_sorts_local_ctx [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
infer_type_wf_env [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
infer_wf_env [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
infer_typing [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
infer_term [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
infer_replacement_inductive [definition, in MetaRocq.Quotation.ToTemplate.Init]
infer_term [definition, in MetaRocq.Template.Checker]
infer_cumul [definition, in MetaRocq.Template.Checker]
infer_type [definition, in MetaRocq.Template.Checker]
infer_spine [definition, in MetaRocq.Template.Checker]
infer_isType [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
infer_type [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
infer' [definition, in MetaRocq.Template.Checker]
inf_cons [constructor, in MetaRocq.PCUIC.Bidirectional.BDTyping]
inh [definition, in MetaRocq.Examples.typing_correctness]
inh [definition, in MetaRocq.Examples.metarocq_tour_prelude]
inhabit_formula [definition, in MetaRocq.Examples.tauto]
InHypUnderBindersDo [library]
Init [library]
Init [library]
init_graph_invariants [lemma, in MetaRocq.Common.uGraph]
init_graph [definition, in MetaRocq.Common.uGraph]
inj_open [definition, in MetaRocq.PCUIC.PCUICContextConversion]
inj_closed [definition, in MetaRocq.PCUIC.PCUICContextConversion]
inj_tags [definition, in MetaRocq.Erasure.EReorderCstrs]
inline [definition, in MetaRocq.Erasure.EInlining]
Inline [section, in MetaRocq.Erasure.EInlining]
inline [definition, in MetaRocq.Erasure.Typed.CertifyingInlining]
inlined_program_inlinings [definition, in MetaRocq.Erasure.EInlining]
inlined_program [definition, in MetaRocq.Erasure.EInlining]
inlined_constants [projection, in MetaRocq.ErasurePlugin.Erasure]
inline_transformation [definition, in MetaRocq.Erasure.EInlining]
inline_program [definition, in MetaRocq.Erasure.EInlining]
inline_env [definition, in MetaRocq.Erasure.EInlining]
inline_add [definition, in MetaRocq.Erasure.EInlining]
inline_decl [definition, in MetaRocq.Erasure.EInlining]
inline_constant_decl [definition, in MetaRocq.Erasure.EInlining]
inline_projections_optimization_pres_app [instance, in MetaRocq.ErasurePlugin.ErasureCorrectness]
inline_projections_optimization_pres [instance, in MetaRocq.ErasurePlugin.ErasureCorrectness]
inline_projections_optimization_extends' [instance, in MetaRocq.ErasurePlugin.ETransform]
inline_projections_optimization_extends [instance, in MetaRocq.ErasurePlugin.ETransform]
inline_projections_optimization [definition, in MetaRocq.ErasurePlugin.ETransform]
inline_def [definition, in MetaRocq.Erasure.Typed.CertifyingInlining]
inline_globals_template [definition, in MetaRocq.Erasure.Typed.CertifyingInlining]
inline_globals [definition, in MetaRocq.Erasure.Typed.CertifyingInlining]
inline_in_decl [definition, in MetaRocq.Erasure.Typed.CertifyingInlining]
inline_context_decl [definition, in MetaRocq.Erasure.Typed.CertifyingInlining]
inline_oib [definition, in MetaRocq.Erasure.Typed.CertifyingInlining]
inline_in_constant_body [definition, in MetaRocq.Erasure.Typed.CertifyingInlining]
inline_aux [definition, in MetaRocq.Erasure.Typed.CertifyingInlining]
inline_const [definition, in MetaRocq.Erasure.Typed.CertifyingInlining]
Inline.inlining [variable, in MetaRocq.Erasure.EInlining]
inlining [definition, in MetaRocq.Erasure.EInlining]
inlining [projection, in MetaRocq.ErasurePlugin.Erasure]
inlining [section, in MetaRocq.Erasure.Typed.CertifyingInlining]
inlining.should_inline [variable, in MetaRocq.Erasure.Typed.CertifyingInlining]
inlining.Σ [variable, in MetaRocq.Erasure.Typed.CertifyingInlining]
InPrim [definition, in MetaRocq.Erasure.EPrimitive]
InPrim_size [lemma, in MetaRocq.Erasure.EInduction]
InPrim_primProp [lemma, in MetaRocq.Erasure.EPrimitive]
inspect [definition, in MetaRocq.Examples.tauto]
inspect [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
inspect [definition, in MetaRocq.Erasure.ErasureFunction]
inspect [definition, in MetaRocq.Erasure.EUnboxing]
inspect [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
inspect_bool [definition, in MetaRocq.Erasure.ErasureFunction]
inspect_nth_error_rename [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
inst [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
Instance [module, in MetaRocq.Common.Universes]
Instances [module, in MetaRocq.Quotation.ToPCUIC.Init]
Instances [module, in MetaRocq.Quotation.ToTemplate.Init]
Instances.default_debug [instance, in MetaRocq.Quotation.ToPCUIC.Init]
Instances.default_debug [instance, in MetaRocq.Quotation.ToTemplate.Init]
Instance.empty [definition, in MetaRocq.Common.Universes]
Instance.eqb [definition, in MetaRocq.Common.Universes]
Instance.equal_upto [definition, in MetaRocq.Common.Universes]
Instance.is_empty [definition, in MetaRocq.Common.Universes]
Instance.t [definition, in MetaRocq.Common.Universes]
instantiated [inductive, in MetaRocq.PCUIC.PCUICFirstorder]
instantiated_typing_spine_firstorder_spine [lemma, in MetaRocq.PCUIC.PCUICFirstorder]
instantiated_sind [definition, in MetaRocq.PCUIC.PCUICFirstorder]
instantiated_rec [definition, in MetaRocq.PCUIC.PCUICFirstorder]
instantiated_ind [definition, in MetaRocq.PCUIC.PCUICFirstorder]
instantiated_rect [definition, in MetaRocq.PCUIC.PCUICFirstorder]
instantiated_tProd [constructor, in MetaRocq.PCUIC.PCUICFirstorder]
instantiated_LetIn [constructor, in MetaRocq.PCUIC.PCUICFirstorder]
instantiated_mkApps [constructor, in MetaRocq.PCUIC.PCUICFirstorder]
instantiate_wf_subslet [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
instantiate_subslet [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
instantiate_minductive [lemma, in MetaRocq.PCUIC.PCUICContexts]
instantiate_params_substP [lemma, in MetaRocq.Template.Typing]
instantiate_params_subst [definition, in MetaRocq.Template.Typing]
instantiate_params_subst_spec_sind [definition, in MetaRocq.Template.Typing]
instantiate_params_subst_spec_ind [definition, in MetaRocq.Template.Typing]
instantiate_params_subst_vdef [constructor, in MetaRocq.Template.Typing]
instantiate_params_subst_vass [constructor, in MetaRocq.Template.Typing]
instantiate_params_subst_nil [constructor, in MetaRocq.Template.Typing]
instantiate_params_subst_spec [inductive, in MetaRocq.Template.Typing]
instantiate_inds [lemma, in MetaRocq.PCUIC.PCUICInductives]
instantiate_cstr_indices [definition, in MetaRocq.PCUIC.PCUICCasesHelper]
inst_case_branch_context_eq [lemma, in MetaRocq.PCUIC.PCUICSR]
inst_subslet [projection, in MetaRocq.PCUIC.PCUICSpine]
inst_ctx_subst [projection, in MetaRocq.PCUIC.PCUICSpine]
inst_case_branch_context_rename [lemma, in MetaRocq.PCUIC.Conversion.PCUICOnFreeVarsConv]
inst_case_predicate_context_rename [lemma, in MetaRocq.PCUIC.Conversion.PCUICOnFreeVarsConv]
inst_mfix [definition, in MetaRocq.PCUIC.PCUICGuardCondition]
inst_prim_type [lemma, in MetaRocq.PCUIC.Typing.PCUICInstTyp]
inst_convSpec [lemma, in MetaRocq.PCUIC.Typing.PCUICInstTyp]
inst_cumulSpec [lemma, in MetaRocq.PCUIC.Typing.PCUICInstTyp]
inst_case_branch_context_inst [lemma, in MetaRocq.PCUIC.Typing.PCUICInstTyp]
inst_case_predicate_context_inst [lemma, in MetaRocq.PCUIC.Typing.PCUICInstTyp]
inst_context_on_free_vars [lemma, in MetaRocq.PCUIC.Typing.PCUICInstTyp]
inst_mutual_inductive_body [definition, in MetaRocq.PCUIC.Syntax.PCUICInstDef]
inst_context_snoc0 [definition, in MetaRocq.PCUIC.Syntax.PCUICInstDef]
inst_decl [definition, in MetaRocq.PCUIC.Syntax.PCUICInstDef]
inst_context_ext [instance, in MetaRocq.PCUIC.Syntax.PCUICInstDef]
inst_context [definition, in MetaRocq.PCUIC.Syntax.PCUICInstDef]
inst_case_predicate_context_alpha_eq [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
inst_case_predicate_context_eq [lemma, in MetaRocq.PCUIC.PCUICAlpha]
inst_closed [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
inst_extended_subst_shift [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_assoc [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_rename_assoc [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_rename_assoc_n [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_mkApps [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_cofix [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_fix [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_letin [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_prod [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_lam [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_app [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_branch_proper [instance, in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_predicate_proper [instance, in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_ext [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_branches [abbreviation, in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_branch [abbreviation, in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_predicate [abbreviation, in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_case_branch_context_eq [lemma, in MetaRocq.PCUIC.PCUICCasesContexts]
inst_case_predicate_context_eq [lemma, in MetaRocq.PCUIC.PCUICCasesContexts]
inst_is_constructor [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
inst_ctxmap_up [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
inst_ctxmap [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
inst_case_branch_context_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
inst_case_predicate_context_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
inst_case_context_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
inst_case_ws_cumul_ctx_pb [lemma, in MetaRocq.PCUIC.PCUICConvCumInversion]
inst_case_branch_context_length [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
inst_case_branch_context [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
inst_case_predicate_context_length [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
inst_case_predicate_context [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
inst_case_context_assumptions [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
inst_case_context_length [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
inst_case_context [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
inst_context_telescope [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_telescope_cons [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_telescope_upn0 [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_telescope_ext [instance, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_subst_telescope [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_telescope [definition, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_cumul_decls [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_conv_decls [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_cumul [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_conv [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_is_open_term [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_on_free_vars [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_ext_cond [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_predicate_set_preturn [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_predicate_set_pparams [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_unfold_cofix [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_unfold_fix [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_iota_red [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_extended_subst [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_wf_cofixpoint [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_wf_fixpoint [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_check_one_cofix [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_check_one_fix [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_smash_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_app_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_decompose_prod_assum [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_case_branch_type [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_case_branch_context_gen [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_cstr_branch_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_inst_case_context_wf [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_inst_case_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_context_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_context_set_binder_name [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_inds [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_context_lift [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_lift [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_closed_extended_subst [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_closedn_terms [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_cstr_args [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_closed_constructor_body [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_closed_decl [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_wf_branches [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_wf_branch [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_wf_predicate [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_case_predicate_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_context_subst [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_context_subst_k [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_subst [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_to_extended_list [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_reln [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_it_mkLambda_or_LetIn [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_mkLambda_or_LetIn [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_predicate_preturn [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_predicate_pcontext [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_fix_context_up [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_fix_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_destArity [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_wf_local [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_closedn_ctx [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_decl_closed [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_ext_closed [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_closed0 [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_subst0 [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_mkApps [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_context_length [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_context_alt [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_context_snoc [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_constructor_body [definition, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_case_branch_context_eq [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
inst_case_predicate_context_eq [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
inst_case_context [definition, in MetaRocq.Template.Ast]
inter_checker_flags_spec [lemma, in MetaRocq.Common.config]
inter_checker_flags [definition, in MetaRocq.Common.config]
IntoAny [constructor, in MetaRocq.Common.Universes]
IntoPropSProp [constructor, in MetaRocq.Common.Universes]
IntoSetPropSProp [constructor, in MetaRocq.Common.Universes]
IntoSProp [constructor, in MetaRocq.Common.Universes]
into_closed_red_ctx [lemma, in MetaRocq.PCUIC.PCUICSR]
into_wt_cumul_ctx_pb [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
into_ws_cumul_decls [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
into_ws_cumul_pb [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
into_ws_cumul_pb_terms_Algo [lemma, in MetaRocq.SafeChecker.PCUICSafeRetyping]
into_ws_cumul_ctx_pb [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
into_ws_cumul_pb_terms [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
into_ws_cumul_ctx_pb_rel [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
into_closed_red [lemma, in MetaRocq.PCUIC.PCUICConversion]
into_ws_cumul [lemma, in MetaRocq.PCUIC.PCUICInversion]
into_red_terms [lemma, in MetaRocq.PCUIC.PCUICConvCumInversion]
introP [lemma, in MetaRocq.Utils.ReflectEq]
introT [lemma, in MetaRocq.Utils.MRReflect]
invariants_proper_iff [instance, in MetaRocq.Common.uGraph]
invariants_proper [instance, in MetaRocq.Common.uGraph]
Inversion [section, in MetaRocq.PCUIC.PCUICInversion]
Inversions [section, in MetaRocq.PCUIC.PCUICConversion]
Inversions [section, in MetaRocq.PCUIC.PCUICConversion]
Inversions.cf [variable, in MetaRocq.PCUIC.PCUICConversion]
Inversions.cf [variable, in MetaRocq.PCUIC.PCUICConversion]
Inversions.wfΣ [variable, in MetaRocq.PCUIC.PCUICConversion]
Inversions.wfΣ [variable, in MetaRocq.PCUIC.PCUICConversion]
Inversions.Σ [variable, in MetaRocq.PCUIC.PCUICConversion]
Inversions.Σ [variable, in MetaRocq.PCUIC.PCUICConversion]
inversion_Rel [lemma, in MetaRocq.Examples.tauto]
inversion_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICSpine]
inversion_mkApps_direct [lemma, in MetaRocq.PCUIC.PCUICSpine]
inversion_mkApps [lemma, in MetaRocq.PCUIC.PCUICValidity]
inversion_it_mkProd_or_LetIn [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
inversion_mkApps [lemma, in MetaRocq.PCUIC.PCUICProgress]
inversion_it_mkLambda_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICInversion]
inversion_Prim [lemma, in MetaRocq.PCUIC.PCUICInversion]
inversion_CoFix [lemma, in MetaRocq.PCUIC.PCUICInversion]
inversion_Fix [lemma, in MetaRocq.PCUIC.PCUICInversion]
inversion_Proj [lemma, in MetaRocq.PCUIC.PCUICInversion]
inversion_Case [lemma, in MetaRocq.PCUIC.PCUICInversion]
inversion_Construct [lemma, in MetaRocq.PCUIC.PCUICInversion]
inversion_Ind [lemma, in MetaRocq.PCUIC.PCUICInversion]
inversion_Const [lemma, in MetaRocq.PCUIC.PCUICInversion]
inversion_App_size [lemma, in MetaRocq.PCUIC.PCUICInversion]
inversion_App [lemma, in MetaRocq.PCUIC.PCUICInversion]
inversion_LetIn [lemma, in MetaRocq.PCUIC.PCUICInversion]
inversion_Lambda [lemma, in MetaRocq.PCUIC.PCUICInversion]
inversion_Prod_size [lemma, in MetaRocq.PCUIC.PCUICInversion]
inversion_Prod [lemma, in MetaRocq.PCUIC.PCUICInversion]
inversion_Sort [lemma, in MetaRocq.PCUIC.PCUICInversion]
inversion_Evar [lemma, in MetaRocq.PCUIC.PCUICInversion]
inversion_Var [lemma, in MetaRocq.PCUIC.PCUICInversion]
inversion_Rel [lemma, in MetaRocq.PCUIC.PCUICInversion]
Inversion.cf [variable, in MetaRocq.PCUIC.PCUICInversion]
Inversion.wfΣ [variable, in MetaRocq.PCUIC.PCUICInversion]
Inversion.Σ [variable, in MetaRocq.PCUIC.PCUICInversion]
invert_cumul_it_mkProd_or_LetIn_Sort_Ind [lemma, in MetaRocq.PCUIC.PCUICFirstorder]
invert_red_mkApps_tRel [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
invert_Proj_Construct [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
invert_Case_Construct [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
invert_red_lambda [lemma, in MetaRocq.PCUIC.PCUICConversion]
invert_cumul_ind_sort [lemma, in MetaRocq.PCUIC.PCUICConversion]
invert_cumul_sort_ind [lemma, in MetaRocq.PCUIC.PCUICConversion]
invert_cumul_ind_ind [lemma, in MetaRocq.PCUIC.PCUICConversion]
invert_cumul_ind_prod [lemma, in MetaRocq.PCUIC.PCUICConversion]
invert_cumul_prod_ind [lemma, in MetaRocq.PCUIC.PCUICConversion]
invert_cumul_Prim [lemma, in MetaRocq.PCUIC.PCUICConversion]
invert_cumul_prim_type_prod [lemma, in MetaRocq.PCUIC.PCUICConversion]
invert_cumul_prim_type_ind [lemma, in MetaRocq.PCUIC.PCUICConversion]
invert_cumul_axiom_prod [lemma, in MetaRocq.PCUIC.PCUICConversion]
invert_cumul_axiom_ind [lemma, in MetaRocq.PCUIC.PCUICConversion]
invert_red_ind [abbreviation, in MetaRocq.PCUIC.PCUICConversion]
invert_red_mkApps_tInd [lemma, in MetaRocq.PCUIC.PCUICConversion]
invert_cumul_arity_l [lemma, in MetaRocq.PCUIC.PCUICConversion]
invert_cumul_arity_r [lemma, in MetaRocq.PCUIC.PCUICConversion]
invert_red_sort [lemma, in MetaRocq.PCUIC.PCUICConversion]
invert_red_tPrim [lemma, in MetaRocq.PCUIC.PCUICConversion]
invert_red_axiom_app [lemma, in MetaRocq.PCUIC.PCUICConversion]
invert_red1_axiom_app [lemma, in MetaRocq.PCUIC.PCUICConversion]
invert_red_axiom [lemma, in MetaRocq.PCUIC.PCUICConversion]
invert_red_prod [lemma, in MetaRocq.PCUIC.PCUICConversion]
invert_red_letin [lemma, in MetaRocq.PCUIC.PCUICConversion]
invert_cumul_arity_l [lemma, in MetaRocq.PCUIC.PCUICArities]
invert_Forall2_dep [definition, in MetaRocq.Utils.All_Forall]
invert_Forall2 [definition, in MetaRocq.Utils.All_Forall]
invert_red1_letin [lemma, in MetaRocq.PCUIC.PCUICInductives]
invert_type_mkApps_ind [lemma, in MetaRocq.PCUIC.PCUICInductives]
invert_fix_ind [lemma, in MetaRocq.PCUIC.PCUICClassification]
invert_ind_ind [lemma, in MetaRocq.PCUIC.PCUICClassification]
invert_cumul_arity_r_gen [lemma, in MetaRocq.PCUIC.PCUICClassification]
invert_cumul_arity_l_gen [lemma, in MetaRocq.PCUIC.PCUICClassification]
invert_it_Ind_eq_prod [lemma, in MetaRocq.Erasure.EArities]
invert_type_mkApps_tProd [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
inv_opt_monad [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
inv_stuck_cofixes [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
inv_stuck_fixes [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
inv_reduced_body_proj [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
inv_reduced_discriminees_case [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
inv_wf_local [lemma, in MetaRocq.SafeChecker.PCUICTypeChecker]
inv_opt_monad [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
inv_on_free_vars_decl [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
In_app_inv [lemma, in MetaRocq.Erasure.Typed.Erasure]
In_size [lemma, in MetaRocq.Utils.MRList]
In_unfold_inj [lemma, in MetaRocq.Utils.MRList]
In_map [lemma, in MetaRocq.PCUIC.PCUICElimination]
in_global_deps_fresh [lemma, in MetaRocq.Erasure.ErasureFunction]
In_skipn [lemma, in MetaRocq.Erasure.ErasureFunction]
in_global_deps [lemma, in MetaRocq.Erasure.ErasureFunction]
in_global_levels [lemma, in MetaRocq.PCUIC.PCUICWeakeningEnv]
In_term_global_deps [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
In_map_All [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
in_deps_in_erase_global_deps [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
in_erase_global_deps_acc [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
In_lift_constraints [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
In_Var_global_ext_poly [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
In_unfold_inj [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
In_list_depth [lemma, in MetaRocq.PCUIC.Syntax.PCUICDepth]
In_Forall [lemma, in MetaRocq.Utils.All_Forall]
In_All [lemma, in MetaRocq.Utils.All_Forall]
In_lookup_globals [lemma, in MetaRocq.Template.TypingWf]
in_global_ext_subst_abs_level [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
in_var_global_ext [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
In_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
In_subst_instance_cstrs' [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
In_subst_instance_cstrs [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
In_unfold_var [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
in_subst_instance [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
In_Level_global_ext_poly [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
iota_body [definition, in MetaRocq.Erasure.Typed.Utils]
iota_red [definition, in MetaRocq.Template.Typing]
iota_red_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
iota_red [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
iota_red [definition, in MetaRocq.Erasure.EGlobalEnv]
irred_equal [lemma, in MetaRocq.PCUIC.PCUICNormalization]
Irrelevant [constructor, in MetaRocq.Common.BasicAst]
isApp [definition, in MetaRocq.PCUIC.PCUICAst]
isApp [definition, in MetaRocq.Erasure.EAst]
isApp [definition, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
isApp [definition, in MetaRocq.Template.Ast]
isAppPrim [definition, in MetaRocq.PCUIC.PCUICSafeLemmata]
isAppPrim_isPrim [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
isAppPrim_mkApps [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
isAppProd [definition, in MetaRocq.PCUIC.PCUICSafeLemmata]
isAppProd_isProd [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
isAppProd_mkApps [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
isApp_false_nApp [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
isApp_mkApps [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
isApp_mkApps [lemma, in MetaRocq.Erasure.ERemoveParams]
isArity [definition, in MetaRocq.PCUIC.PCUICTyping]
isArity [definition, in MetaRocq.Template.Typing]
isArityHead [definition, in MetaRocq.Template.WcbvEval]
isArityHead [definition, in MetaRocq.PCUIC.PCUICWcbvEval]
isArityHead_mkApps [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
isArity_mkNormalArity [lemma, in MetaRocq.Erasure.Typed.Erasure]
isArity_red [lemma, in MetaRocq.Erasure.Typed.Erasure]
isArity_red [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
isArity_mkAssumArity [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
isArity_trans [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
isArity_subst_instance [lemma, in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
isArity_red1 [lemma, in MetaRocq.PCUIC.PCUICConversion]
isArity_subst [lemma, in MetaRocq.PCUIC.PCUICConversion]
isArity_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICArities]
isArity_ind [lemma, in MetaRocq.PCUIC.PCUICClassification]
isArity_typing_spine [lemma, in MetaRocq.PCUIC.PCUICClassification]
isArity_subst [lemma, in MetaRocq.PCUIC.PCUICClassification]
isArity_mkApps [lemma, in MetaRocq.Erasure.EArities]
isArity_ind_type [lemma, in MetaRocq.Erasure.EArities]
isAssRel [definition, in MetaRocq.Template.WcbvEval]
isAssRel [definition, in MetaRocq.PCUIC.PCUICWcbvEval]
isAxiom [definition, in MetaRocq.Template.WcbvEval]
isAxiom [definition, in MetaRocq.PCUIC.PCUICWcbvEval]
isBox [definition, in MetaRocq.Erasure.EAstUtils]
isBox_csubst [lemma, in MetaRocq.Erasure.ECSubst]
isBox_remove_match_on_box [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
isBox_optimize [lemma, in MetaRocq.Erasure.EReorderCstrs]
isBox_mkApps [lemma, in MetaRocq.Erasure.EWcbvEval]
isBox_optimize [lemma, in MetaRocq.Erasure.EInlineProjections]
isBox_mkApps [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
isBox_mkApps_Construct [lemma, in MetaRocq.Erasure.ERemoveParams]
isBox_mkApps' [lemma, in MetaRocq.Erasure.ERemoveParams]
isBox_lift [lemma, in MetaRocq.Erasure.ELiftSubst]
isBox_trans [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
isCoFinite [definition, in MetaRocq.PCUIC.PCUICTyping]
isCoFinite [definition, in MetaRocq.Template.Typing]
isCoFix [definition, in MetaRocq.Template.WcbvEval]
isCoFix [definition, in MetaRocq.Template.Checker]
isCoFix [definition, in MetaRocq.PCUIC.PCUICWcbvEval]
isCoFix [definition, in MetaRocq.Erasure.EAstUtils]
isCoFix_app [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
isConstruct [definition, in MetaRocq.Template.WcbvEval]
isConstruct [definition, in MetaRocq.Template.EtaExpand]
isConstruct [definition, in MetaRocq.PCUIC.PCUICEtaExpand]
isConstruct [definition, in MetaRocq.Template.Checker]
isConstruct [definition, in MetaRocq.PCUIC.PCUICWcbvEval]
isConstruct [definition, in MetaRocq.Erasure.EAstUtils]
isConstructApp [definition, in MetaRocq.Template.WcbvEval]
isConstructApp [definition, in MetaRocq.PCUIC.PCUICWcbvEval]
isConstructApp [definition, in MetaRocq.Erasure.EAstUtils]
isConstructApp_mkApps [lemma, in MetaRocq.Template.WcbvEval]
isConstructApp_trans [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
isConstructApp_mkApps [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
isConstructApp_mkApps [lemma, in MetaRocq.Erasure.EAstUtils]
isConstruct_app_ne [lemma, in MetaRocq.PCUIC.PCUICNormal]
isConstruct_app_eq_term_r [lemma, in MetaRocq.PCUIC.PCUICEquality]
isConstruct_app_eq_term_l [lemma, in MetaRocq.PCUIC.PCUICEquality]
isConstruct_app [definition, in MetaRocq.Template.AstUtils]
isConstruct_app [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
isConstruct_erase [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
isConstruct_app_rename [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
isConstruct_app_pred1 [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
isConstruct_app_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
isConstruct_app_inst [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
isconv [definition, in MetaRocq.Template.Checker]
isconv [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_prog [definition, in MetaRocq.Template.Checker]
isconv_term_complete [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_term_sound [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_term [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_complete [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_sound [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_full [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_array_values [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_array_values_aux [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_predicate [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_predicate_params [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_predicate_params_aux [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_branches' [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_branches [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_context [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_context_aux [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_fallback [abbreviation, in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_args [abbreviation, in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_prog [abbreviation, in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_red [abbreviation, in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_fallback_raw [abbreviation, in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_args_raw [abbreviation, in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_prog_raw [abbreviation, in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_red_raw [abbreviation, in MetaRocq.SafeChecker.PCUICSafeConversion]
isErasable [definition, in MetaRocq.Erasure.Extract]
isErasable_subst_instance [lemma, in MetaRocq.Erasure.ErasureProperties]
isErasable_irrel_global_env [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
isErasable_lets [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
isErasable_red [lemma, in MetaRocq.Erasure.EArities]
isErasable_unfold_cofix [lemma, in MetaRocq.Erasure.EArities]
isErasable_Propositional [lemma, in MetaRocq.Erasure.EArities]
isErasable_any_type [lemma, in MetaRocq.Erasure.EArities]
isErasable_Type [definition, in MetaRocq.Erasure.EArities]
isErasable_Proof [lemma, in MetaRocq.Erasure.EArities]
isEtaExp [abbreviation, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp [abbreviation, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp [section, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp [definition, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp [section, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp [definition, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp [section, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExpFix_env_isEtaExp_env [lemma, in MetaRocq.Erasure.EEtaExpanded]
isEtaExpFix_isEtaExp [lemma, in MetaRocq.Erasure.EEtaExpanded]
isEtaExpFix_tApp_arg [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_mkApps [lemma, in MetaRocq.Erasure.EUnboxing]
isEtaExp_tApp_arg [lemma, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_env_expanded_global_env [lemma, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_expanded [lemma, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_app_expanded [lemma, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_lookup [lemma, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_extends_decl [lemma, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_extends [lemma, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_app_extends [lemma, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_lookup_ext [lemma, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_env [definition, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_decl [definition, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_constant_decl [definition, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_cunfold_cofix [lemma, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_cunfold_fix [lemma, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_cofix_subst [lemma, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_fix_subst [lemma, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_iota_red [lemma, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_substl [lemma, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_mkApps_intro [lemma, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_app_mon [lemma, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_tApp [lemma, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_mkApps_intro_notConstruct [lemma, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_mkApps [lemma, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_Constructor [lemma, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_mkApps_napp [lemma, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_mkApps_nonnil [lemma, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_app [definition, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_lift [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_iota_red' [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_closedn [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_tApp_eval [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_tFix [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_FixApp [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_fixapp_mon [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_lookup [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_extends_decl [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_extends [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_app_extends [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_lookup_ext [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_tApp' [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_env [definition, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_decl [definition, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_constant_decl [definition, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_expanded [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_app_expanded [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_tApp [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_cunfold_cofix [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_cunfold_fix [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_cofix_subst [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_iota_red [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_fixsubstl [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_substl [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_closed [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_mkApps_intro [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_Constructor [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_mkApps [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_mkApps_nonnil [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_app_mon [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_fixapp [definition, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_app [definition, in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_dearg_single_construct [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
isEtaExp_dearg_single [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
isEtaExp_dearg_lambdas [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
isEtaExp_dearg_case_branch_body_rec [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
isEtaExp_mkApps [lemma, in MetaRocq.Erasure.ERemoveParams]
isEtaExp.Σ [variable, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp.Σ [variable, in MetaRocq.Erasure.EEtaExpanded]
isEtaExp.Σ [variable, in MetaRocq.Erasure.EEtaExpandedFix]
isEvar [definition, in MetaRocq.Template.WcbvEval]
isEvar [definition, in MetaRocq.PCUIC.PCUICWcbvEval]
isEvar [definition, in MetaRocq.Erasure.EAstUtils]
isFinite [definition, in MetaRocq.PCUIC.PCUICTyping]
isFinite [definition, in MetaRocq.Template.Typing]
isFix [definition, in MetaRocq.Template.WcbvEval]
isFix [definition, in MetaRocq.Template.EtaExpand]
isFix [definition, in MetaRocq.PCUIC.PCUICEtaExpand]
isFix [definition, in MetaRocq.PCUIC.PCUICWcbvEval]
isFix [definition, in MetaRocq.Erasure.EAstUtils]
isFixApp [definition, in MetaRocq.Template.WcbvEval]
isFixApp [definition, in MetaRocq.PCUIC.PCUICConversion]
isFixApp [definition, in MetaRocq.PCUIC.PCUICWcbvEval]
isFixApp [definition, in MetaRocq.Erasure.EAstUtils]
isFixApp_mkApps [lemma, in MetaRocq.Template.WcbvEval]
isFixApp_trans [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
isFixApp_trans [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
isFixApp_mkApps [lemma, in MetaRocq.PCUIC.PCUICConversion]
isFixApp_mkApps [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
isFixApp_mkApps [lemma, in MetaRocq.Erasure.EAstUtils]
isFixLambda [definition, in MetaRocq.PCUIC.Syntax.PCUICViews]
isFixLambda_app_rename [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
isFixLambda_app_mkApps' [lemma, in MetaRocq.PCUIC.Syntax.PCUICViews]
isFixLambda_app_mkApps [lemma, in MetaRocq.PCUIC.Syntax.PCUICViews]
isFixLambda_app [definition, in MetaRocq.PCUIC.Syntax.PCUICViews]
isFix_app [definition, in MetaRocq.Template.EtaExpand]
isFix_mkApps [lemma, in MetaRocq.Erasure.EGenericGlobalMap]
isFix_mkApps [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
isFix_mkApps [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
isFix_mkApps [lemma, in MetaRocq.Erasure.EGenericMapEnv]
isFix_mkApps [lemma, in MetaRocq.Erasure.EReorderCstrs]
isFix_mkApps [lemma, in MetaRocq.Erasure.EInlineProjections]
isFix_mkApps_Construct [lemma, in MetaRocq.Erasure.ERemoveParams]
isFix_mkApps' [lemma, in MetaRocq.Erasure.ERemoveParams]
isFix_mkApps [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
isFunction [definition, in MetaRocq.ErasurePlugin.ErasureCorrectness]
isInd [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
isInd [definition, in MetaRocq.PCUIC.PCUICWcbvEval]
isIndConstructApp [definition, in MetaRocq.PCUIC.PCUICConvCumInversion]
isIndConstructApp_mkApps [lemma, in MetaRocq.PCUIC.PCUICConvCumInversion]
isLambda [definition, in MetaRocq.PCUIC.PCUICAst]
isLambda [definition, in MetaRocq.Erasure.EAst]
isLambda [definition, in MetaRocq.Template.Ast]
isLambda_eq_term_r [lemma, in MetaRocq.PCUIC.PCUICEquality]
isLambda_eq_term_l [lemma, in MetaRocq.PCUIC.PCUICEquality]
isLambda_subst [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
isLambda_lift [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
isLambda_implement_box [lemma, in MetaRocq.Erasure.EImplementBox]
isLambda_subst_instance [lemma, in MetaRocq.Erasure.ErasureProperties]
isLambda_csubst [lemma, in MetaRocq.Erasure.ECSubst]
isLambda_inv [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
isLambda_eta_expand [lemma, in MetaRocq.Template.EtaExpand]
isLambda_unlift [lemma, in MetaRocq.Template.EtaExpand]
isLambda_subst [lemma, in MetaRocq.Template.LiftSubst]
isLambda_lift [lemma, in MetaRocq.Template.LiftSubst]
isLambda_red1 [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
isLambda_mkApps [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
isLambda_isApp [lemma, in MetaRocq.Template.WfAst]
isLambda_rename [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
isLambda_inv [lemma, in MetaRocq.PCUIC.PCUICAst]
isLambda_remove_match_on_box [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
isLambda_optimize [lemma, in MetaRocq.Erasure.EReorderCstrs]
isLambda_transform_blocks [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
isLambda_mkApps [lemma, in MetaRocq.Erasure.EWcbvEval]
isLambda_optimize [lemma, in MetaRocq.Erasure.EInlineProjections]
isLambda_mkApps [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
isLambda_mkApps_Construct [lemma, in MetaRocq.Erasure.ERemoveParams]
isLambda_mkApps' [lemma, in MetaRocq.Erasure.ERemoveParams]
isLambda_subst [lemma, in MetaRocq.Erasure.ELiftSubst]
isLambda_lift [lemma, in MetaRocq.Erasure.ELiftSubst]
isLambda_trans [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
isLazy [definition, in MetaRocq.Erasure.EAstUtils]
isLazyApp [definition, in MetaRocq.Erasure.EAstUtils]
isLazyApp_mkApps [lemma, in MetaRocq.Erasure.EAstUtils]
IsLeibniz [module, in MetaRocq.Utils.MRMSets]
IsLeibniz.eq_leibniz [axiom, in MetaRocq.Utils.MRMSets]
IsLtIrrel [module, in MetaRocq.Utils.MRMSets]
IsLtIrrel.lt_irrel [axiom, in MetaRocq.Utils.MRMSets]
isPrim [definition, in MetaRocq.PCUIC.PCUICSafeLemmata]
isPrim [definition, in MetaRocq.Template.WcbvEval]
isPrim [definition, in MetaRocq.PCUIC.PCUICWcbvEval]
isPrim [definition, in MetaRocq.Erasure.EAstUtils]
isPrimApp [definition, in MetaRocq.PCUIC.PCUICWcbvEval]
isPrimApp [definition, in MetaRocq.Erasure.EAstUtils]
isPrimApp_trans [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
isPrimApp_mkApps [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
isPrimApp_mkApps [lemma, in MetaRocq.Erasure.EAstUtils]
isPrimmkApps [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
isPrim_mkApps [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
isProd [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
isProdmkApps [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
isPropositional [definition, in MetaRocq.PCUIC.PCUICFirstorder]
isPropositionalArity [definition, in MetaRocq.PCUIC.PCUICFirstorder]
isPropositional_propositional_cstr [lemma, in MetaRocq.Erasure.EArities]
isPropositional_propositional [lemma, in MetaRocq.Erasure.EArities]
isprop_ind [definition, in MetaRocq.Erasure.EOptimizePropDiscr]
isred [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
isred_full_nobeta [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
isred_full [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
isRel [definition, in MetaRocq.Template.EtaExpand]
isRel [definition, in MetaRocq.PCUIC.PCUICEtaExpand]
isRel [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
isRel [definition, in MetaRocq.Erasure.EAstUtils]
isRel_app [definition, in MetaRocq.Template.EtaExpand]
isRel_n [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
isSome [definition, in MetaRocq.Erasure.EWellformed]
isSort [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
isSort [definition, in MetaRocq.Template.Typing]
isSortmkApps [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
isStackApp [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
isStackApp_false_appstack [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
isStuckFix [definition, in MetaRocq.Template.WcbvEval]
isStuckFix [definition, in MetaRocq.Erasure.EWcbvEval]
isStuckFix [definition, in MetaRocq.PCUIC.PCUICWcbvEval]
isStuckfix_nApp [lemma, in MetaRocq.Template.WcbvEval]
isStuckfix_nApp [lemma, in MetaRocq.Erasure.EWcbvEval]
isStuckfix_nApp [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
isStuckFix' [definition, in MetaRocq.Erasure.EEtaExpandedFix]
istrue_proper [instance, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
isTT [definition, in MetaRocq.Erasure.Typed.Erasure]
isTypebd_isType [lemma, in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
isType_prod_cod [lemma, in MetaRocq.Erasure.Typed.Erasure]
isType_prod_dom [lemma, in MetaRocq.Erasure.Typed.Erasure]
isType_red_sq [lemma, in MetaRocq.Erasure.Typed.Erasure]
isType_tLetIn [lemma, in MetaRocq.PCUIC.PCUICSR]
isType_red [lemma, in MetaRocq.PCUIC.PCUICSR]
isType_red1 [lemma, in MetaRocq.PCUIC.PCUICSR]
isType_mkApps_Ind_proj_inv [lemma, in MetaRocq.PCUIC.PCUICSR]
isType_subst_extended_subst [lemma, in MetaRocq.PCUIC.PCUICSR]
isType_expand_lets [lemma, in MetaRocq.PCUIC.PCUICSR]
isType_subst_arities [lemma, in MetaRocq.PCUIC.PCUICSR]
isType_weaken [lemma, in MetaRocq.PCUIC.PCUICSR]
isType_lift [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningTyp]
isType_substitution [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
isType_closedPT [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
isType_wf_local [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
isType_ws_cumul_ctx_pb [lemma, in MetaRocq.PCUIC.PCUICElimination]
isType_it_mkProd_or_LetIn_app [lemma, in MetaRocq.PCUIC.PCUICSpine]
isType_context_conversion [lemma, in MetaRocq.PCUIC.PCUICFirstorder]
isType_ws_cumul_pb_refl [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
isType_open [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
isType_welltyped [definition, in MetaRocq.PCUIC.PCUICTyping]
isType_weakening [lemma, in MetaRocq.PCUIC.PCUICValidity]
isType_subst_instance_decl [lemma, in MetaRocq.PCUIC.PCUICValidity]
isType_Sort_inv [lemma, in MetaRocq.PCUIC.PCUICValidity]
isType_extends [lemma, in MetaRocq.PCUIC.PCUICValidity]
isType_weaken_full [lemma, in MetaRocq.PCUIC.PCUICValidity]
isType_wt [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
isType_subst_instance_id [lemma, in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
isType_subst_instance_decl [lemma, in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
isType_all_rels_subst_lift [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
isType_subst_all_rels [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
isType_is_open_term [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
isType_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
isType_mkApps_Ind_smash [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
isType_weaken [lemma, in MetaRocq.PCUIC.PCUICArities]
isType_it_mkProd_or_LetIn_wf_local [lemma, in MetaRocq.PCUIC.PCUICArities]
isType_substitution_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICArities]
isType_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICArities]
isType_apply [lemma, in MetaRocq.PCUIC.PCUICArities]
isType_tLetIn_dom [lemma, in MetaRocq.PCUIC.PCUICArities]
isType_tLetIn_red [lemma, in MetaRocq.PCUIC.PCUICArities]
isType_subst_gen [lemma, in MetaRocq.PCUIC.PCUICArities]
isType_subst [lemma, in MetaRocq.PCUIC.PCUICArities]
isType_tProd [lemma, in MetaRocq.PCUIC.PCUICArities]
isType_Sort [lemma, in MetaRocq.PCUIC.PCUICArities]
isType_alpha_ctx [lemma, in MetaRocq.PCUIC.PCUICAlpha]
isType_alpha [lemma, in MetaRocq.PCUIC.PCUICAlpha]
isType_eq_context_conversion [lemma, in MetaRocq.PCUIC.PCUICAlpha]
isType_it_mkProd [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
isType_tSort [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
isType_mkApps_inv [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
isType_it_mkProd_or_LetIn_inv [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
isType_infering_sort [lemma, in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
isType_case_predicate [lemma, in MetaRocq.PCUIC.PCUICInductives]
isType_mkApps_Ind_inv' [lemma, in MetaRocq.PCUIC.PCUICInductives]
isType_mkApps_Ind_inv [lemma, in MetaRocq.PCUIC.PCUICInductives]
isType_it_mkProd_or_LetIn_smash [lemma, in MetaRocq.PCUIC.PCUICInductives]
isType_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICInductives]
isType_it_mkProd_or_LetIn_subst [lemma, in MetaRocq.PCUIC.PCUICInductives]
isType_it_mkProd_or_LetIn_inv [lemma, in MetaRocq.PCUIC.PCUICInductives]
isType_mkApps_Ind [lemma, in MetaRocq.PCUIC.PCUICInductives]
isType_intro [lemma, in MetaRocq.PCUIC.PCUICInductives]
isType_on_ctx_free_vars [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
isType_on_free_vars [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
isType_closed_red_refl [lemma, in MetaRocq.Erasure.EArities]
isType_red [lemma, in MetaRocq.Erasure.EArities]
isType_isErasable [lemma, in MetaRocq.Erasure.EArities]
isType_wf_universes [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
isType_mkApps_Ind_smash_inv [lemma, in MetaRocq.SafeChecker.PCUICTypeChecker]
isType_mkApps_Ind_smash [lemma, in MetaRocq.SafeChecker.PCUICTypeChecker]
isType_wt [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
isType_mkApps_Ind_inv_spine [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
isType_is_open_term [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
isType_closed [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
isType_mkApps_Ind_inv_spine [lemma, in MetaRocq.PCUIC.PCUICCasesHelper]
isType_lift [lemma, in MetaRocq.PCUIC.PCUICCasesHelper]
isType_it_mkProd [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
isType_tSort [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
isWAT [abbreviation, in MetaRocq.PCUIC.PCUICArities]
iswellinferred [constructor, in MetaRocq.SafeChecker.PCUICSafeRetyping]
iswelltyped [constructor, in MetaRocq.PCUIC.PCUICTyping]
isWfArity [definition, in MetaRocq.PCUIC.PCUICTyping]
isWfArity_red [lemma, in MetaRocq.PCUIC.PCUICSR]
isWfArity_red1 [lemma, in MetaRocq.PCUIC.PCUICSR]
isWfArity_subst_instance_decl [lemma, in MetaRocq.PCUIC.PCUICValidity]
isWfArity_alpha [lemma, in MetaRocq.PCUIC.PCUICAlpha]
isWfArity_prod_inv [lemma, in MetaRocq.Erasure.EArities]
isWfArity_sort [lemma, in MetaRocq.PCUIC.PCUICPrincipality]
isws_cumul_pb_Fix [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
isws_cumul_pb_fix_bodies [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
isws_cumul_pb_fix_types [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
is_constructor_app_false [lemma, in MetaRocq.PCUIC.PCUICNormal]
is_logical [projection, in MetaRocq.Erasure.Typed.Erasure]
is_arity [definition, in MetaRocq.Erasure.Typed.Erasure]
Is_conv_to_Arity_conv_arity [lemma, in MetaRocq.Erasure.Typed.Erasure]
is_sort [definition, in MetaRocq.Erasure.Typed.Erasure]
Is_conv_to_Sort [definition, in MetaRocq.Erasure.Typed.Erasure]
is_prod_or_sort [definition, in MetaRocq.Erasure.Typed.Erasure]
is_open_term_snoc [lemma, in MetaRocq.PCUIC.PCUICSR]
is_closed_context_set_binder_name [lemma, in MetaRocq.PCUIC.PCUICSR]
is_assumption_context_spec [lemma, in MetaRocq.Erasure.Prelim]
is_leaf_sound [lemma, in MetaRocq.Examples.tauto]
is_leaf [definition, in MetaRocq.Examples.tauto]
Is_conv_to_Arity_red [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
is_prefix_rev_is_suffix [lemma, in MetaRocq.Utils.MRList]
is_suffix_is_prefix_rev [lemma, in MetaRocq.Utils.MRList]
is_suffix [definition, in MetaRocq.Utils.MRList]
is_prefix_cons_inv [lemma, in MetaRocq.Utils.MRList]
is_prefix_cons [lemma, in MetaRocq.Utils.MRList]
is_prefix_nil [lemma, in MetaRocq.Utils.MRList]
is_prefix [definition, in MetaRocq.Utils.MRList]
Is_proof_mkApps_tConstruct [lemma, in MetaRocq.PCUIC.PCUICElimination]
is_propositional_subst_instance [lemma, in MetaRocq.PCUIC.PCUICElimination]
Is_proof [definition, in MetaRocq.PCUIC.PCUICElimination]
is_empty_type_decl [definition, in MetaRocq.Erasure.Typed.Extraction]
is_allowed_elimination_monotone [lemma, in MetaRocq.Common.Universes]
is_allowed_elimination [definition, in MetaRocq.Common.Universes]
is_lSet [definition, in MetaRocq.Common.Universes]
is_allowed_elimination_cuniv [definition, in MetaRocq.Common.Universes]
is_propositional_or_set [definition, in MetaRocq.Common.Universes]
is_sprop_sort_prod [lemma, in MetaRocq.Common.Universes]
is_prop_sort_prod [lemma, in MetaRocq.Common.Universes]
is_type_sup_r [lemma, in MetaRocq.Common.Universes]
is_sprop_sup_iff [lemma, in MetaRocq.Common.Universes]
is_prop_sup [lemma, in MetaRocq.Common.Universes]
is_prop_or_sprop_sort_sup_prop [lemma, in MetaRocq.Common.Universes]
is_prop_sort_sup_prop [lemma, in MetaRocq.Common.Universes]
is_prop_or_sprop_sort_sup [lemma, in MetaRocq.Common.Universes]
is_prop_sort_sup' [lemma, in MetaRocq.Common.Universes]
is_prop_sort_sup [lemma, in MetaRocq.Common.Universes]
is_not_prop_and_is_not_sprop [lemma, in MetaRocq.Common.Universes]
is_prop_and_is_sprop_val_false [lemma, in MetaRocq.Common.Universes]
is_sprop_val [lemma, in MetaRocq.Common.Universes]
is_prop_val [lemma, in MetaRocq.Common.Universes]
is_declared_cstr_levels [definition, in MetaRocq.Common.Universes]
is_closed_context_smash_end [lemma, in MetaRocq.PCUIC.PCUICSpine]
is_fresh [definition, in MetaRocq.Template.Pretty]
is_erasableb_irrel_global_env [lemma, in MetaRocq.Erasure.ErasureFunction]
is_arity_irrel [lemma, in MetaRocq.Erasure.ErasureFunction]
is_erasableb_irrel [lemma, in MetaRocq.Erasure.ErasureFunction]
is_erasable [definition, in MetaRocq.Erasure.ErasureFunction]
is_erasableP [lemma, in MetaRocq.Erasure.ErasureFunction]
is_erasableb [definition, in MetaRocq.Erasure.ErasureFunction]
is_arityP [lemma, in MetaRocq.Erasure.ErasureFunction]
is_arity [definition, in MetaRocq.Erasure.ErasureFunction]
is_ind_app_head_mkApps [lemma, in MetaRocq.Template.AstUtils]
is_ind_app_head [definition, in MetaRocq.Template.AstUtils]
is_empty_app [lemma, in MetaRocq.Template.AstUtils]
is_empty [definition, in MetaRocq.Template.AstUtils]
Is_type_conv_context [lemma, in MetaRocq.Erasure.ErasureProperties]
is_PrimApp_erases [lemma, in MetaRocq.Erasure.ErasureProperties]
is_ConstructApp_erases [lemma, in MetaRocq.Erasure.ErasureProperties]
is_FixApp_erases [lemma, in MetaRocq.Erasure.ErasureProperties]
is_propositional_cstr_unbox [lemma, in MetaRocq.Erasure.EUnboxing]
is_propositional_unbox [lemma, in MetaRocq.Erasure.EUnboxing]
is_unboxable [definition, in MetaRocq.Erasure.EUnboxing]
is_allowed_elimination_dec [definition, in MetaRocq.Common.UniversesDec]
is_lSet_dec [definition, in MetaRocq.Common.UniversesDec]
is_nil [lemma, in MetaRocq.Template.WcbvEval]
is_box_or_any [definition, in MetaRocq.Erasure.Typed.Optimize]
is_expanded_env [definition, in MetaRocq.Erasure.Typed.Optimize]
is_expanded [definition, in MetaRocq.Erasure.Typed.Optimize]
is_expanded_aux [definition, in MetaRocq.Erasure.Typed.Optimize]
is_dead [definition, in MetaRocq.Erasure.Typed.Optimize]
is_ind_app_head_mkApps [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
is_ind_app_head [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
is_nil [definition, in MetaRocq.Erasure.EEtaExpanded]
is_truev [projection, in MetaRocq.Quotation.CommonUtils]
is_truev [constructor, in MetaRocq.Quotation.CommonUtils]
is_supermodule_of [definition, in MetaRocq.Quotation.ToPCUIC.Init]
is_submodule_of [definition, in MetaRocq.Quotation.ToPCUIC.Init]
is_closed_context_cumul_app [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
is_fo [constructor, in MetaRocq.Erasure.ErasureFunctionProperties]
is_closed_context_cstr_branch_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
is_closed_context_subst [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
is_assumption_context_spec [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
is_propositional_cstr_gen_transform [lemma, in MetaRocq.Erasure.EGenericGlobalMap]
is_propositional_gen_transform [lemma, in MetaRocq.Erasure.EGenericGlobalMap]
is_closed_context_weaken [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
is_closed_subst_inst [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
is_open_term_subst_instance [lemma, in MetaRocq.PCUIC.PCUICConversion]
is_closed_context_subst_instance [lemma, in MetaRocq.PCUIC.PCUICConversion]
is_open_term_lift [lemma, in MetaRocq.PCUIC.PCUICConversion]
is_closed_context_lift [lemma, in MetaRocq.PCUIC.PCUICConversion]
is_open_fix_onone2 [lemma, in MetaRocq.PCUIC.PCUICConversion]
is_open_fix_or_cofix [lemma, in MetaRocq.PCUIC.PCUICConversion]
is_open_mfix [abbreviation, in MetaRocq.PCUIC.PCUICConversion]
is_open_def [abbreviation, in MetaRocq.PCUIC.PCUICConversion]
is_open_brs_OnOne2 [lemma, in MetaRocq.PCUIC.PCUICConversion]
is_open_case_set_preturn [lemma, in MetaRocq.PCUIC.PCUICConversion]
is_open_case_set_pparams [lemma, in MetaRocq.PCUIC.PCUICConversion]
is_open_case_split [lemma, in MetaRocq.PCUIC.PCUICConversion]
is_open_case [definition, in MetaRocq.PCUIC.PCUICConversion]
is_open_predicate [abbreviation, in MetaRocq.PCUIC.PCUICConversion]
is_open_brs [abbreviation, in MetaRocq.PCUIC.PCUICConversion]
Is_conv_to_Arity_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
Is_conv_to_Arity [definition, in MetaRocq.PCUIC.PCUICConversion]
is_open_term_subst [lemma, in MetaRocq.PCUIC.PCUICConversion]
is_open_term_subst_gen [lemma, in MetaRocq.PCUIC.PCUICConversion]
is_closed_subst_context [lemma, in MetaRocq.PCUIC.PCUICConversion]
is_fresh [definition, in MetaRocq.PCUIC.utils.PCUICPretty]
is_closed_context_app_right [lemma, in MetaRocq.PCUIC.PCUICAlpha]
is_closed_context_app_left [lemma, in MetaRocq.PCUIC.PCUICAlpha]
is_constructor_rename [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
is_eta_fix_app_map [definition, in MetaRocq.ErasurePlugin.ErasureCorrectness]
is_eta_fix_app [definition, in MetaRocq.ErasurePlugin.ErasureCorrectness]
is_eta_app_map [definition, in MetaRocq.ErasurePlugin.ErasureCorrectness]
is_eta_app [definition, in MetaRocq.ErasurePlugin.ErasureCorrectness]
is_vdef [definition, in MetaRocq.ErasurePlugin.ErasureCorrectness]
is_eta_application_sind [definition, in MetaRocq.ErasurePlugin.ErasureCorrectness]
is_eta_application_ind [definition, in MetaRocq.ErasurePlugin.ErasureCorrectness]
is_eta_application [inductive, in MetaRocq.ErasurePlugin.ErasureCorrectness]
is_eta_fix_application_sind [definition, in MetaRocq.ErasurePlugin.ErasureCorrectness]
is_eta_fix_application_ind [definition, in MetaRocq.ErasurePlugin.ErasureCorrectness]
is_eta_fix_application [inductive, in MetaRocq.ErasurePlugin.ErasureCorrectness]
is_fo_block [constructor, in MetaRocq.ErasurePlugin.ErasureCorrectness]
is_cons [definition, in MetaRocq.Erasure.EEtaExpandedFix]
is_nil [definition, in MetaRocq.Erasure.EEtaExpandedFix]
is_type_subst [lemma, in MetaRocq.Erasure.ESubstitution]
Is_type_weakening [lemma, in MetaRocq.Erasure.ESubstitution]
Is_proof_extends [lemma, in MetaRocq.Erasure.ESubstitution]
Is_type_extends [lemma, in MetaRocq.Erasure.ESubstitution]
is_propositional_cstr_remove_match_on_box [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
is_propositional_remove_match_on_box [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
is_box_inv [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
is_graph_of_uctx_proper [instance, in MetaRocq.SafeChecker.PCUICSafeChecker]
is_supermodule_of [definition, in MetaRocq.Quotation.ToTemplate.Init]
is_submodule_of [definition, in MetaRocq.Quotation.ToTemplate.Init]
is_propositional_cstr_gen_transform [lemma, in MetaRocq.Erasure.EGenericMapEnv]
is_propositional_gen_transform [lemma, in MetaRocq.Erasure.EGenericMapEnv]
is_propositional_cstr_optimize [lemma, in MetaRocq.Erasure.EReorderCstrs]
is_propositional_optimize [lemma, in MetaRocq.Erasure.EReorderCstrs]
is_nil [definition, in MetaRocq.Template.TemplateCheckWf]
is_constructor [definition, in MetaRocq.Template.Typing]
is_graph_of_global_env_ext [definition, in MetaRocq.Template.Checker]
is_none [definition, in MetaRocq.Erasure.Typed.Certifying]
is_closed_context_expand_let [lemma, in MetaRocq.PCUIC.PCUICInductives]
is_closed_context_weaken [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
is_closed_context_snoc_inv [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
is_sprop_prod [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
is_prop_prod [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
is_sprop_superE [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
is_prop_superE [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
is_sprop_bottom [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
is_prop_bottom [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
is_propositional_bottom [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
is_constructor_pred1 [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
is_fresh [definition, in MetaRocq.Erasure.EPretty]
is_nil [definition, in MetaRocq.Erasure.EWellformed]
is_axiom_decl [definition, in MetaRocq.Erasure.Extract]
is_propositional_cstr_optimize [lemma, in MetaRocq.Erasure.EInlineProjections]
is_propositional_optimize [lemma, in MetaRocq.Erasure.EInlineProjections]
Is_conv_to_Arity_ind [lemma, in MetaRocq.PCUIC.PCUICClassification]
is_allowed_elimination_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
is_monomorphic_cstr [definition, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
is_prop_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
is_sprop_subst_instance_univ [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
is_prop_subst_instance_univ [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
is_propositional_subst_instance_univ [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Is_proof_app [lemma, in MetaRocq.Erasure.EArities]
Is_proof_ind [lemma, in MetaRocq.Erasure.EArities]
is_propositional_lower [lemma, in MetaRocq.Erasure.EArities]
is_propositional_bottom [lemma, in MetaRocq.Erasure.EArities]
is_propositional_bottom' [lemma, in MetaRocq.Erasure.EArities]
Is_proof_ty [lemma, in MetaRocq.Erasure.EArities]
Is_type_eval_inv [lemma, in MetaRocq.Erasure.EArities]
Is_type_eval [lemma, in MetaRocq.Erasure.EArities]
Is_type_red [lemma, in MetaRocq.Erasure.EArities]
Is_type_lambda [lemma, in MetaRocq.Erasure.EArities]
is_propositional_sort_prod [lemma, in MetaRocq.Erasure.EArities]
Is_type_app [lemma, in MetaRocq.Erasure.EArities]
is_expanded_constant [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_expanded_cunfold_cofix [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_expanded_cunfold_fix [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_expanded_substl [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_expanded_aux_subst [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_expanded_csubst [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_expanded_aux_upwards [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_expanded_aux_mkApps [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_expanded_aux_mkApps_inv [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_expanded_mkApps_eq [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_expanded_aux_mkApps_eq [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_dead_dearg_aux [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_dead_dearg_case [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_dead_dearg_branch_body [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_dead_dearg_lambdas [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_dead_subst [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_dead_dearg_single [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_dead_lift [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_dead_mkApps [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_expanded_lift [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_expanded_aux_lift [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_dead_subst_other [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_dead_lift_all [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_dead_lift_other [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_expanded_env [abbreviation, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_expanded [abbreviation, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_expanded_aux [abbreviation, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_dead_csubst [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_dead_closed [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_constructor_prefix [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
is_constructor_app_ge [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
is_constructor [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
is_consistent_spec2 [lemma, in MetaRocq.Common.uGraph]
is_graph_of_uctx_add [lemma, in MetaRocq.Common.uGraph]
is_graph_of_uctx_levels [lemma, in MetaRocq.Common.uGraph]
is_graph_of_uctx_proper [instance, in MetaRocq.Common.uGraph]
is_acyclic_proper [instance, in MetaRocq.Common.uGraph]
is_graph_of_uctx [definition, in MetaRocq.Common.uGraph]
is_lt_spec [lemma, in MetaRocq.Common.uGraph]
is_lt [definition, in MetaRocq.Common.uGraph]
is_consistent_spec [lemma, in MetaRocq.Common.uGraph]
is_consistent [definition, in MetaRocq.Common.uGraph]
is_nth_constructor_app_or_box [definition, in MetaRocq.Erasure.EGlobalEnv]
is_constructor_app_or_box [definition, in MetaRocq.Erasure.EGlobalEnv]
is_constructor_inst [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
is_propositional_cstr_strip [lemma, in MetaRocq.Erasure.ERemoveParams]
is_propositional_strip [lemma, in MetaRocq.Erasure.ERemoveParams]
is_closed_context [abbreviation, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
is_open_decl [abbreviation, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
is_open_term [abbreviation, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
is_closed_ctx_closed [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
is_open_term_closed [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
is_graph_of_uctx_levels [lemma, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
is_propositional_cstr_trans [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
is_propositional_trans [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
is_box_inv [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
is_box_tApp [lemma, in MetaRocq.Erasure.EAstUtils]
is_box_mkApps [lemma, in MetaRocq.Erasure.EAstUtils]
is_box [definition, in MetaRocq.Erasure.EAstUtils]
iter [definition, in MetaRocq.Erasure.ErasureFunction]
IteratedBetaReduction [section, in MetaRocq.PCUIC.PCUICConversion]
IteratedBetaReduction.cf [variable, in MetaRocq.PCUIC.PCUICConversion]
iter_abstract_pop_decls_correct [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
it_mkProd_or_LetIn_inj [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
it_mkLambda_or_LetIn_inj [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
it_mkLambda_or_LetIn_welltyped [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
it_mkLambda_or_LetIn_app [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
it_mkProd_or_LetIn_wf_local [lemma, in MetaRocq.PCUIC.PCUICArities]
it_mkProd_or_LetIn_inj [lemma, in MetaRocq.Template.TypingWf]
it_mkProd_red_Arity [lemma, in MetaRocq.Erasure.EArities]
it_mkProd_arity [lemma, in MetaRocq.Erasure.EArities]
it_mkProd_isArity [lemma, in MetaRocq.Erasure.EArities]
it_mkLambda_or_LetIn [definition, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
it_mkLambda_or_LetIn_app [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]

---

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

(19204 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

(228 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

(298 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

(1273 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

(313 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

(8163 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

(1514 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

(52 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

(352 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

(534 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

(727 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

(402 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

(333 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

(4833 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

(182 entries)

Generated by coqdoc and improved with CoqdocJS