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)

---

F

Fa [constructor, in MetaRocq.Examples.tauto]
fail_nf [definition, in MetaRocq.Template.TemplateMonad.Core]
fake_params_length [lemma, in MetaRocq.PCUIC.PCUICNormal]
fake_params [definition, in MetaRocq.PCUIC.PCUICNormal]
fake_guard_impl_instance [instance, in MetaRocq.Erasure.Typed.Erasure]
fake_guard_impl [definition, in MetaRocq.Erasure.Typed.Erasure]
fake_guard_impl [instance, in MetaRocq.Examples.typing_correctness]
fake_abstract_guard_impl [instance, in MetaRocq.SafeCheckerPlugin.Extraction]
fake_abstract_guard_impl_properties [axiom, in MetaRocq.SafeCheckerPlugin.Extraction]
fake_normalization [axiom, in MetaRocq.ErasurePlugin.Erasure]
fake_guard_impl [instance, in MetaRocq.ErasurePlugin.Erasure]
fake_guard_impl_properties [axiom, in MetaRocq.ErasurePlugin.Erasure]
fake_guard_impl [instance, in MetaRocq.Examples.metarocq_tour_prelude]
fake_params [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fake_guard_impl [definition, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
Fallback [constructor, in MetaRocq.SafeChecker.PCUICSafeConversion]
False_FinitelyListablePackage [instance, in MetaRocq.Utils.MRListable]
False_mib [definition, in MetaRocq.PCUIC.PCUICConsistency]
False_oib [definition, in MetaRocq.PCUIC.PCUICConsistency]
Fast [module, in MetaRocq.Erasure.ERemoveParams]
Fast.faststrip [section, in MetaRocq.Erasure.ERemoveParams]
Fast.faststrip.Σ [variable, in MetaRocq.Erasure.ERemoveParams]
Fast.strip [definition, in MetaRocq.Erasure.ERemoveParams]
Fast.strip_env_fast [lemma, in MetaRocq.Erasure.ERemoveParams]
Fast.strip_env [definition, in MetaRocq.Erasure.ERemoveParams]
Fast.strip_decl [definition, in MetaRocq.Erasure.ERemoveParams]
Fast.strip_inductive_decl [definition, in MetaRocq.Erasure.ERemoveParams]
Fast.strip_constant_decl [definition, in MetaRocq.Erasure.ERemoveParams]
Fast.strip_fast [lemma, in MetaRocq.Erasure.ERemoveParams]
Fast.strip_acc_opt [lemma, in MetaRocq.Erasure.ERemoveParams]
Fast.strip_defs [definition, in MetaRocq.Erasure.ERemoveParams]
Fast.strip_brs [definition, in MetaRocq.Erasure.ERemoveParams]
Fast.strip_args [definition, in MetaRocq.Erasure.ERemoveParams]
Fast.strip' [abbreviation, in MetaRocq.Erasure.ERemoveParams]
fill_context_hole_inj [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
fill_hole [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
fill_branches_hole [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
fill_predicate_hole [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
fill_context_hole [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
fill_mfix_hole [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
fill_eq [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
fill_le [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
fill_pb [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
fill_mkApps_context [lemma, in MetaRocq.PCUIC.PCUICReduction]
fill_branch_context [definition, in MetaRocq.PCUIC.PCUICReduction]
fill_list_context [definition, in MetaRocq.PCUIC.PCUICReduction]
fill_context [definition, in MetaRocq.PCUIC.PCUICReduction]
filter_length [lemma, in MetaRocq.Utils.MRList]
filter_deps_filter [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
filter_deps [definition, in MetaRocq.Erasure.ErasureFunctionProperties]
filter_deps_ext [lemma, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
final_wcbv_flags [definition, in MetaRocq.ErasurePlugin.Erasure]
FindHyp [library]
find_index_inj [lemma, in MetaRocq.Utils.MRListable]
find_index_iff [lemma, in MetaRocq.Utils.MRListable]
find_index_ok [projection, in MetaRocq.Utils.MRListable]
find_index [projection, in MetaRocq.Utils.MRListable]
find_tag_wf [lemma, in MetaRocq.Erasure.EReorderCstrs]
find_tag_None [lemma, in MetaRocq.Erasure.EReorderCstrs]
find_tag [definition, in MetaRocq.Erasure.EReorderCstrs]
Finite [constructor, in MetaRocq.Common.BasicAst]
FinitelyListable [record, in MetaRocq.Utils.MRListable]
FinitelyListablePackage [record, in MetaRocq.Utils.MRListable]
FinitelyListablePackage_FinitelyListable [projection, in MetaRocq.Utils.MRListable]
FinitelyListablePackage_Listable [projection, in MetaRocq.Utils.MRListable]
firstn_length_le_inv [lemma, in MetaRocq.Utils.MRList]
firstn_app_left [lemma, in MetaRocq.Utils.MRList]
firstn_app_left_rem [lemma, in MetaRocq.Utils.MRList]
firstn_add [lemma, in MetaRocq.Utils.MRList]
firstn_firstn_firstn [lemma, in MetaRocq.Utils.MRList]
firstn_0 [lemma, in MetaRocq.Utils.MRList]
firstn_ge [lemma, in MetaRocq.Utils.MRList]
firstn_map [lemma, in MetaRocq.Utils.MRList]
firstn_all_app_eq [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
firstn_subst_context [lemma, in MetaRocq.PCUIC.PCUICClassification]
firstorder [section, in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_value_irred [lemma, in MetaRocq.PCUIC.PCUICNormalization]
firstorder_value_alpha [lemma, in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_value_spec [lemma, in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_args [lemma, in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_mutind_ext [lemma, in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_spine_let [lemma, in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_spine_sind [definition, in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_spine_rec [definition, in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_spine_ind [definition, in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_spine_rect [definition, in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_spine_cons [constructor, in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_spine_nil [constructor, in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_spine [inductive, in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_ind_propositional [lemma, in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_value_inds [lemma, in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_value_sind [definition, in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_value_ind [definition, in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_value_C [constructor, in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_value [inductive, in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_lookup_inv [lemma, in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_env [definition, in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_env' [definition, in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_ind [definition, in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_mutind [definition, in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_oneind [definition, in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_con [definition, in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_type [definition, in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_evalue_extends [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
firstorder_erases_deterministic [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
firstorder_evalue_elim [definition, in MetaRocq.Erasure.ErasureFunctionProperties]
firstorder_evalue_sind [definition, in MetaRocq.Erasure.ErasureFunctionProperties]
firstorder_evalue_ind [definition, in MetaRocq.Erasure.ErasureFunctionProperties]
firstorder_evalue [inductive, in MetaRocq.Erasure.ErasureFunctionProperties]
firstorder_evalue_block_transform [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
firstorder_evalue_block_elim [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
firstorder_evalue_block_sind [definition, in MetaRocq.ErasurePlugin.ErasureCorrectness]
firstorder_evalue_block_ind [definition, in MetaRocq.ErasurePlugin.ErasureCorrectness]
firstorder_evalue_block [inductive, in MetaRocq.ErasurePlugin.ErasureCorrectness]
firstorder.Σ [variable, in MetaRocq.PCUIC.PCUICFirstorder]
firstorder.Σb [variable, in MetaRocq.PCUIC.PCUICFirstorder]
Fix [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
Fix [constructor, in MetaRocq.PCUIC.PCUICTyping]
FixCoFix [inductive, in MetaRocq.PCUIC.PCUICTyping]
FixCoFix_sind [definition, in MetaRocq.PCUIC.PCUICTyping]
FixCoFix_rec [definition, in MetaRocq.PCUIC.PCUICTyping]
FixCoFix_ind [definition, in MetaRocq.PCUIC.PCUICTyping]
FixCoFix_rect [definition, in MetaRocq.PCUIC.PCUICTyping]
fixed [section, in MetaRocq.PCUIC.PCUICConvCumInversion]
fixed.cf [variable, in MetaRocq.PCUIC.PCUICConvCumInversion]
fixed.wfΣ [variable, in MetaRocq.PCUIC.PCUICConvCumInversion]
fixed.Σ [variable, in MetaRocq.PCUIC.PCUICConvCumInversion]
FixMfixMismatch [constructor, in MetaRocq.SafeChecker.PCUICErrors]
FixRargMismatch [constructor, in MetaRocq.SafeChecker.PCUICErrors]
FixSigmaExt [section, in MetaRocq.Erasure.Typed.Erasure]
FixSigmaExt.no [variable, in MetaRocq.Erasure.Typed.Erasure]
FixSigmaExt.normalization_in [variable, in MetaRocq.Erasure.Typed.Erasure]
FixSigmaExt.rΣ [variable, in MetaRocq.Erasure.Typed.Erasure]
FixSigmaExt.wfrΣ [variable, in MetaRocq.Erasure.Typed.Erasure]
FixSigmaExt.X [variable, in MetaRocq.Erasure.Typed.Erasure]
FixSigmaExt.X_type [variable, in MetaRocq.Erasure.Typed.Erasure]
fix_context_fix_context_alt [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
fix_context_alt [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
Fix_app [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
fix_mfix_bd [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
fix_mfix_ty [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
fix_subst_nth [lemma, in MetaRocq.Erasure.Prelim]
fix_context_pres_let_bodies [lemma, in MetaRocq.PCUIC.PCUICRedTypeIrrelevance]
fix_context_gen [definition, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
Fix_F_prop [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
fix_context [definition, in MetaRocq.Template.Pretty]
fix_sigma.normalization_in [variable, in MetaRocq.Erasure.ErasureFunction]
fix_sigma.X [variable, in MetaRocq.Erasure.ErasureFunction]
fix_sigma.X_type [variable, in MetaRocq.Erasure.ErasureFunction]
fix_sigma.nor [variable, in MetaRocq.Erasure.ErasureFunction]
fix_sigma.cf [variable, in MetaRocq.Erasure.ErasureFunction]
fix_sigma [section, in MetaRocq.Erasure.ErasureFunction]
fix_guard_rename [definition, in MetaRocq.PCUIC.PCUICGuardCondition]
fix_guard_inst [definition, in MetaRocq.PCUIC.PCUICGuardCondition]
fix_guard_context_cumulativity [definition, in MetaRocq.PCUIC.PCUICGuardCondition]
fix_guard_extends [definition, in MetaRocq.PCUIC.PCUICGuardCondition]
fix_guard_subst_instance [definition, in MetaRocq.PCUIC.PCUICGuardCondition]
fix_guard_eq_term [definition, in MetaRocq.PCUIC.PCUICGuardCondition]
fix_guard_red1 [definition, in MetaRocq.PCUIC.PCUICGuardCondition]
fix_guard [definition, in MetaRocq.PCUIC.PCUICTyping]
fix_context_subst_instance [lemma, in MetaRocq.Erasure.ErasureProperties]
fix_env.annotate.annotate_types [variable, in MetaRocq.Erasure.Typed.TypeAnnotations]
fix_env.annotate.A [variable, in MetaRocq.Erasure.Typed.TypeAnnotations]
fix_env.annotate [section, in MetaRocq.Erasure.Typed.TypeAnnotations]
fix_env.wfextΣ [variable, in MetaRocq.Erasure.Typed.TypeAnnotations]
fix_env.Σ [variable, in MetaRocq.Erasure.Typed.TypeAnnotations]
fix_env [section, in MetaRocq.Erasure.Typed.TypeAnnotations]
fix_flags.wfl [variable, in MetaRocq.Erasure.Typed.WcbvEvalAux]
fix_flags [section, in MetaRocq.Erasure.Typed.WcbvEvalAux]
fix_guard_trans [axiom, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
fix_or_cofix [definition, in MetaRocq.PCUIC.PCUICConversion]
fix_context_nth_error [lemma, in MetaRocq.PCUIC.PCUICAlpha]
fix_lambda_view_sind [definition, in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_lambda_view_rec [definition, in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_lambda_view_ind [definition, in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_lambda_view_rect [definition, in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_lambda_other [constructor, in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_lambda_fix [constructor, in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_lambda_lambda [constructor, in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_lambda_view [inductive, in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_lambda_app_view_sind [definition, in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_lambda_app_view_rec [definition, in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_lambda_app_view_ind [definition, in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_lambda_app_view_rect [definition, in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_lambda_app_other [constructor, in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_lambda_app_lambda [constructor, in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_lambda_app_fix [constructor, in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_lambda_app_view [inductive, in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_test.test [variable, in MetaRocq.PCUIC.PCUICAst]
fix_test [section, in MetaRocq.PCUIC.PCUICAst]
fix_guard_extends [projection, in MetaRocq.Template.Typing]
fix_guard_subst_instance [projection, in MetaRocq.Template.Typing]
fix_guard_subst [projection, in MetaRocq.Template.Typing]
fix_guard_lift [projection, in MetaRocq.Template.Typing]
fix_guard_red1 [projection, in MetaRocq.Template.Typing]
fix_guard [projection, in MetaRocq.Template.Typing]
fix_red_body [constructor, in MetaRocq.Template.Typing]
fix_red_ty [constructor, in MetaRocq.Template.Typing]
fix_context_length [lemma, in MetaRocq.Template.Typing]
fix_context [definition, in MetaRocq.Template.Typing]
fix_subst_length [lemma, in MetaRocq.Template.Typing]
fix_subst [definition, in MetaRocq.Template.Typing]
fix_decls [definition, in MetaRocq.Template.Checker]
fix_red_body [constructor, in MetaRocq.PCUIC.PCUICReduction]
fix_red_ty [constructor, in MetaRocq.PCUIC.PCUICReduction]
fix_context_map_fix [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fix_context_fold [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fix_context_assumption_context [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fix_context_gen_assumption_context [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fix_env_length [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
fix_env [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
fix_sigma.normalization_in [variable, in MetaRocq.SafeChecker.PCUICWfReduction]
fix_sigma.X [variable, in MetaRocq.SafeChecker.PCUICWfReduction]
fix_sigma.X_type [variable, in MetaRocq.SafeChecker.PCUICWfReduction]
fix_sigma.no [variable, in MetaRocq.SafeChecker.PCUICWfReduction]
fix_sigma.cf [variable, in MetaRocq.SafeChecker.PCUICWfReduction]
fix_sigma [section, in MetaRocq.SafeChecker.PCUICWfReduction]
fix_sigma.HΣ [variable, in MetaRocq.SafeChecker.PCUICWfReduction]
fix_sigma.normalization [variable, in MetaRocq.SafeChecker.PCUICWfReduction]
fix_sigma.Σ [variable, in MetaRocq.SafeChecker.PCUICWfReduction]
fix_sigma.no [variable, in MetaRocq.SafeChecker.PCUICWfReduction]
fix_sigma.cf [variable, in MetaRocq.SafeChecker.PCUICWfReduction]
fix_sigma [section, in MetaRocq.SafeChecker.PCUICWfReduction]
fix_app_is_constructor [lemma, in MetaRocq.PCUIC.PCUICClassification]
fix_context_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
fix_subst_instance_subst [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
fix_subst_dearg [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
fix_context_length [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
fix_subst_length [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
fix_subst [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
fix_kind_sind [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
fix_kind_rec [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
fix_kind_ind [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
fix_kind_rect [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
fix_kind [inductive, in MetaRocq.SafeChecker.PCUICSafeConversion]
fix_guard_trans [axiom, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
fix_subst_length [lemma, in MetaRocq.Erasure.EGlobalEnv]
fix_subst [definition, in MetaRocq.Erasure.EGlobalEnv]
fix_guard_trans [axiom, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
flags_after_projs [definition, in MetaRocq.Erasure.EInlineProjections]
flag_of_type [definition, in MetaRocq.Erasure.Typed.Erasure]
flag_of_type_impl [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
Flip [section, in MetaRocq.Utils.MRRelations]
flip_PreOrder [lemma, in MetaRocq.PCUIC.PCUICConfluence]
flip_Transitive [lemma, in MetaRocq.Utils.MRRelations]
flip_Symmetric [lemma, in MetaRocq.Utils.MRRelations]
flip_Reflexive [lemma, in MetaRocq.Utils.MRRelations]
Flip.A [variable, in MetaRocq.Utils.MRRelations]
Flip.R [variable, in MetaRocq.Utils.MRRelations]
float64_to_model [definition, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
float64_model [definition, in MetaRocq.Common.BasicAst]
float64_from_model [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplate]
FMapAVL [module, in MetaRocq.Utils.MRFSets]
FMapAVL.Decide [module, in MetaRocq.Utils.MRFSets]
FMapAVL.DecideSig [module, in MetaRocq.Utils.MRFSets]
FMapAVL.Decide.Raw [module, in MetaRocq.Utils.MRFSets]
FMapAVL.Decide.Raw.bst_dec [definition, in MetaRocq.Utils.MRFSets]
FMapAVL.Decide.Raw.gt_tree_dec [definition, in MetaRocq.Utils.MRFSets]
FMapAVL.Decide.Raw.lt_tree_dec [definition, in MetaRocq.Utils.MRFSets]
FMapAVL.Decide.Raw.with_t.elt [variable, in MetaRocq.Utils.MRFSets]
FMapAVL.Decide.Raw.with_t [section, in MetaRocq.Utils.MRFSets]
FMapAVL.MakeSig [module, in MetaRocq.Utils.MRFSets]
FMapList [module, in MetaRocq.Utils.MRFSets]
FMapList.RawSig [module, in MetaRocq.Utils.MRFSets]
FoldFix [section, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
FoldFix.rho [variable, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
FoldFix.Γ [variable, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fold_left_andb_forallb [lemma, in MetaRocq.Utils.MRList]
fold_left_i [definition, in MetaRocq.Utils.MRList]
fold_left_i_aux [definition, in MetaRocq.Utils.MRList]
fold_left_eq [lemma, in MetaRocq.Erasure.ErasureFunction]
fold_termM [definition, in MetaRocq.Template.AstUtils]
fold_term [definition, in MetaRocq.Template.AstUtils]
fold_term_with_bindersM [definition, in MetaRocq.Template.AstUtils]
fold_branch_with_bindersM [definition, in MetaRocq.Template.AstUtils]
fold_predicate_with_bindersM [definition, in MetaRocq.Template.AstUtils]
fold_term_with_binders [definition, in MetaRocq.Template.AstUtils]
fold_branch_with_binders [definition, in MetaRocq.Template.AstUtils]
fold_predicate_with_binders [definition, in MetaRocq.Template.AstUtils]
fold_lefti [definition, in MetaRocq.Erasure.Typed.Optimize]
fold_context_k_defs_length [lemma, in MetaRocq.Template.EtaExpand]
fold_context_k_defs [definition, in MetaRocq.Template.EtaExpand]
fold_right_ext [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
fold_right_map [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
fold_context_k_map_comm [lemma, in MetaRocq.Common.BasicAst]
fold_context_k_map [lemma, in MetaRocq.Common.BasicAst]
fold_context_k_proper [instance, in MetaRocq.Common.BasicAst]
fold_context_k_ext [lemma, in MetaRocq.Common.BasicAst]
fold_context_k_compose [lemma, in MetaRocq.Common.BasicAst]
fold_context_k_id [lemma, in MetaRocq.Common.BasicAst]
fold_context_Proper [instance, in MetaRocq.Common.BasicAst]
fold_context_In_spec [lemma, in MetaRocq.Common.BasicAst]
fold_context_length [lemma, in MetaRocq.Common.BasicAst]
fold_context [definition, in MetaRocq.Common.BasicAst]
fold_context_In [definition, in MetaRocq.Common.BasicAst]
fold_context_k_app [lemma, in MetaRocq.Common.BasicAst]
fold_context_k_snoc0 [lemma, in MetaRocq.Common.BasicAst]
fold_context_k_length [lemma, in MetaRocq.Common.BasicAst]
fold_context_k_tip [lemma, in MetaRocq.Common.BasicAst]
fold_context_k_alt [lemma, in MetaRocq.Common.BasicAst]
fold_context_k [definition, in MetaRocq.Common.BasicAst]
fold_max_le' [lemma, in MetaRocq.Utils.wGraph]
fold_max_le [lemma, in MetaRocq.Utils.wGraph]
fold_max_In [lemma, in MetaRocq.Utils.wGraph]
fold_context_cst [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fold_fix_context_alt [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fold_fix_context_rho_ctx [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fold_fix_context_over_acc [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fold_context_mapi_context [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fold_fix_context_app [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fold_fix_context_rev [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fold_fix_context_rev_mapi [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fold_fix_context_wf_fold [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fold_fix_context_wf [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fold_context_term [abbreviation, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fold_fix_context_length [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fold_fix_context [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fold_left_add_gc_Some_subset [lemma, in MetaRocq.Common.uGraph]
fold_left_add_gc_None [lemma, in MetaRocq.Common.uGraph]
fold_left_comm_ext3 [lemma, in MetaRocq.Common.uGraph]
fold_left_comm_ext2 [lemma, in MetaRocq.Common.uGraph]
fold_left_comm_ext [lemma, in MetaRocq.Common.uGraph]
fold_left_max_spec' [lemma, in MetaRocq.Common.uGraph]
fold_left_max_spec [lemma, in MetaRocq.Common.uGraph]
fold_left_false [lemma, in MetaRocq.Common.uGraph]
fold_right_xpred0 [lemma, in MetaRocq.Common.uGraph]
fold_prim [definition, in MetaRocq.Erasure.EPrimitive]
foo [definition, in MetaRocq.Examples.metarocq_tour]
forallbi [definition, in MetaRocq.Erasure.Typed.Optimize]
forallbi [definition, in MetaRocq.ErasurePlugin.ErasureCorrectness]
forallbi_impl [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
forallbi_Alli [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
forallbi_Alli [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
forallbi_nth_error [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
forallbP [lemma, in MetaRocq.Utils.All_Forall]
forallbP_cond [lemma, in MetaRocq.Utils.All_Forall]
forallb_repeat [lemma, in MetaRocq.Utils.MRList]
forallb_InP_spec [lemma, in MetaRocq.Utils.MRList]
forallb_InP [definition, in MetaRocq.Utils.MRList]
forallb_mapi [lemma, in MetaRocq.Utils.MRList]
forallb_unfold [lemma, in MetaRocq.Utils.MRList]
forallb_rev [lemma, in MetaRocq.Utils.MRList]
forallb_true [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
forallb_proper [instance, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
forallb_mapi_ext [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
forallb_closed_upwards [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
forallb_forallbi [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
forallb_mapi_forallbi [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
forallb_last [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
forallb_remove_last [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
forallb_firstn [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
forallb_iff [lemma, in MetaRocq.Utils.All_Forall]
forallb_impl [lemma, in MetaRocq.Utils.All_Forall]
forallb_nth' [lemma, in MetaRocq.Utils.All_Forall]
forallb_nth [lemma, in MetaRocq.Utils.All_Forall]
forallb_skipn [lemma, in MetaRocq.Utils.All_Forall]
forallb_Forall' [lemma, in MetaRocq.Utils.All_Forall]
forallb_mapi_impl [lemma, in MetaRocq.Utils.All_Forall]
forallb_mapi [lemma, in MetaRocq.Utils.All_Forall]
forallb_map [lemma, in MetaRocq.Utils.All_Forall]
forallb_All [lemma, in MetaRocq.Utils.All_Forall]
forallb_nth_error [lemma, in MetaRocq.Utils.All_Forall]
forallb_proper [instance, in MetaRocq.Utils.All_Forall]
forallb_ext [lemma, in MetaRocq.Utils.All_Forall]
forallb_Forall [lemma, in MetaRocq.Utils.All_Forall]
forallb_in [lemma, in MetaRocq.Common.uGraph]
forallb_spec [lemma, in MetaRocq.Common.uGraph]
forallb_map_spec [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
forallb2 [definition, in MetaRocq.Utils.All_Forall]
Forallb2 [section, in MetaRocq.Utils.All_Forall]
forallb2P [lemma, in MetaRocq.Utils.All_Forall]
forallb2_Forall2 [lemma, in MetaRocq.Utils.All_Forall]
forallb2_length [lemma, in MetaRocq.Utils.All_Forall]
forallb2_app [lemma, in MetaRocq.Utils.All_Forall]
forallb2_All2 [lemma, in MetaRocq.Utils.All_Forall]
forallb2_map [lemma, in MetaRocq.Utils.All_Forall]
forallb2_refl [lemma, in MetaRocq.Utils.All_Forall]
forallb2_proper [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
Forallb2.A [variable, in MetaRocq.Utils.All_Forall]
Forallb2.B [variable, in MetaRocq.Utils.All_Forall]
Forallb2.f [variable, in MetaRocq.Utils.All_Forall]
forallb3 [definition, in MetaRocq.Utils.All_Forall]
Forallb3 [section, in MetaRocq.Utils.All_Forall]
forallb3P [lemma, in MetaRocq.Utils.All_Forall]
forallb3_Forall3 [lemma, in MetaRocq.Utils.All_Forall]
forallb3_All3 [lemma, in MetaRocq.Utils.All_Forall]
Forallb3.A [variable, in MetaRocq.Utils.All_Forall]
Forallb3.B [variable, in MetaRocq.Utils.All_Forall]
Forallb3.C [variable, in MetaRocq.Utils.All_Forall]
Forallb3.f [variable, in MetaRocq.Utils.All_Forall]
Forall_Forall2_diag [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
Forall_mapi [lemma, in MetaRocq.Erasure.Typed.TypeAnnotations]
Forall_filter [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
Forall_typing_spine_Forall [lemma, in MetaRocq.Template.EtaExpand]
Forall_erases_deps_cofix_subst [lemma, in MetaRocq.Erasure.EDeps]
Forall_erases_deps_fix_subst [lemma, in MetaRocq.Erasure.EDeps]
forall_nth_error_All2i [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
Forall_existsb_false [lemma, in MetaRocq.Erasure.Typed.Utils]
Forall_repeat [lemma, in MetaRocq.Erasure.Typed.Utils]
Forall_snoc [lemma, in MetaRocq.Erasure.Typed.Utils]
Forall_Forall2_and' [lemma, in MetaRocq.Utils.All_Forall]
Forall_Forall2_and [lemma, in MetaRocq.Utils.All_Forall]
Forall_True [lemma, in MetaRocq.Utils.All_Forall]
Forall_Forall2 [lemma, in MetaRocq.Utils.All_Forall]
Forall_forallb [lemma, in MetaRocq.Utils.All_Forall]
Forall_forallb_eq_forallb [lemma, in MetaRocq.Utils.All_Forall]
Forall_last [lemma, in MetaRocq.Utils.All_Forall]
Forall_app [lemma, in MetaRocq.Utils.All_Forall]
Forall_impl [lemma, in MetaRocq.Utils.All_Forall]
Forall_impl_Forall [lemma, in MetaRocq.Utils.All_Forall]
Forall_map_inv [lemma, in MetaRocq.Utils.All_Forall]
Forall_map [lemma, in MetaRocq.Utils.All_Forall]
forall_forallb_forallb_spec [lemma, in MetaRocq.Utils.All_Forall]
forall_forallb_map_spec [lemma, in MetaRocq.Utils.All_Forall]
forall_nth_error_Alli [lemma, in MetaRocq.Utils.All_Forall]
forall_nth_error_All [lemma, in MetaRocq.Utils.All_Forall]
Forall_All [lemma, in MetaRocq.Utils.All_Forall]
Forall_firstn [lemma, in MetaRocq.Utils.All_Forall]
Forall_skipn [lemma, in MetaRocq.Utils.All_Forall]
Forall_mix [lemma, in MetaRocq.Utils.All_Forall]
forall_map_id_spec [lemma, in MetaRocq.Utils.All_Forall]
forall_map_spec [lemma, in MetaRocq.Utils.All_Forall]
Forall_typing_spine_sind [definition, in MetaRocq.Template.Typing]
Forall_typing_spine_rec [definition, in MetaRocq.Template.Typing]
Forall_typing_spine_ind [definition, in MetaRocq.Template.Typing]
Forall_typing_spine_rect [definition, in MetaRocq.Template.Typing]
Forall_type_spine_cons [constructor, in MetaRocq.Template.Typing]
Forall_type_spine_nil [constructor, in MetaRocq.Template.Typing]
Forall_typing_spine [inductive, in MetaRocq.Template.Typing]
Forall_elements_in [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
Forall_decls_on_global_wf [lemma, in MetaRocq.Template.TypingWf]
Forall_closed_repeat_tBox [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
Forall_masked [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
Forall_valid_cases_cofix_subst [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
Forall_valid_cases_fix_subst [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
Forall_closed_cofix_subst [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
Forall_closed_fix_subst [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
Forall_is_expanded_cofix_subst [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
Forall_is_expanded_fix_subst [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
Forall_In [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
Forall_nth_def [lemma, in MetaRocq.SafeChecker.PCUICTypeChecker]
forall_decls_declared_projection [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
forall_decls_declared_constructor [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
forall_decls_declared_inductive [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
forall_decls_declared_minductive [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
forall_decls_declared_constant [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Forall2_ext [instance, in MetaRocq.PCUIC.PCUICEquality]
Forall2_forallb2 [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
Forall2_nth_error_left [lemma, in MetaRocq.Erasure.EDeps]
Forall2_Forall2_Forall3 [lemma, in MetaRocq.Utils.All_Forall]
Forall2_sym [lemma, in MetaRocq.Utils.All_Forall]
Forall2_same [lemma, in MetaRocq.Utils.All_Forall]
Forall2_map' [lemma, in MetaRocq.Utils.All_Forall]
Forall2_eq [lemma, in MetaRocq.Utils.All_Forall]
Forall2_symP [lemma, in MetaRocq.Utils.All_Forall]
Forall2_dep_nth_error [lemma, in MetaRocq.Utils.All_Forall]
Forall2_dep_from_nth_error [lemma, in MetaRocq.Utils.All_Forall]
Forall2_nth_error [lemma, in MetaRocq.Utils.All_Forall]
Forall2_from_nth_error [lemma, in MetaRocq.Utils.All_Forall]
Forall2_Forall_right [lemma, in MetaRocq.Utils.All_Forall]
Forall2_mapi [lemma, in MetaRocq.Utils.All_Forall]
Forall2_rev [lemma, in MetaRocq.Utils.All_Forall]
Forall2_trans [lemma, in MetaRocq.Utils.All_Forall]
Forall2_nth_error_None_l [lemma, in MetaRocq.Utils.All_Forall]
Forall2_nth_error_Some_r [lemma, in MetaRocq.Utils.All_Forall]
Forall2_nth_error_Some_l [lemma, in MetaRocq.Utils.All_Forall]
Forall2_nth [lemma, in MetaRocq.Utils.All_Forall]
Forall2_and [lemma, in MetaRocq.Utils.All_Forall]
Forall2_map_right [lemma, in MetaRocq.Utils.All_Forall]
Forall2_map [lemma, in MetaRocq.Utils.All_Forall]
Forall2_True [lemma, in MetaRocq.Utils.All_Forall]
Forall2_Forall [lemma, in MetaRocq.Utils.All_Forall]
Forall2_impl' [lemma, in MetaRocq.Utils.All_Forall]
Forall2_impl [lemma, in MetaRocq.Utils.All_Forall]
Forall2_nth_error_Some [lemma, in MetaRocq.Utils.All_Forall]
Forall2_skipn [lemma, in MetaRocq.Utils.All_Forall]
Forall2_tip_l [lemma, in MetaRocq.Utils.All_Forall]
Forall2_map_inv [lemma, in MetaRocq.Utils.All_Forall]
Forall2_app_r [lemma, in MetaRocq.Utils.All_Forall]
Forall2_triv [lemma, in MetaRocq.Utils.All_Forall]
Forall2_length [lemma, in MetaRocq.Utils.All_Forall]
Forall2_non_nil [lemma, in MetaRocq.Utils.All_Forall]
Forall2_right [lemma, in MetaRocq.Utils.All_Forall]
Forall2_undep [lemma, in MetaRocq.Utils.All_Forall]
Forall2_All2 [lemma, in MetaRocq.Utils.All_Forall]
Forall2_dep_rec [definition, in MetaRocq.Utils.All_Forall]
Forall2_dep_rect [definition, in MetaRocq.Utils.All_Forall]
Forall2_rec [definition, in MetaRocq.Utils.All_Forall]
Forall2_rect [definition, in MetaRocq.Utils.All_Forall]
Forall2_dep_sind [definition, in MetaRocq.Utils.All_Forall]
Forall2_dep_ind [definition, in MetaRocq.Utils.All_Forall]
Forall2_dep_cons [constructor, in MetaRocq.Utils.All_Forall]
Forall2_dep_nil [constructor, in MetaRocq.Utils.All_Forall]
Forall2_dep [inductive, in MetaRocq.Utils.All_Forall]
Forall3 [inductive, in MetaRocq.Utils.All_Forall]
Forall3_map [lemma, in MetaRocq.Utils.All_Forall]
Forall3_map_inv [lemma, in MetaRocq.Utils.All_Forall]
Forall3_antisymP [lemma, in MetaRocq.Utils.All_Forall]
Forall3_transP [lemma, in MetaRocq.Utils.All_Forall]
Forall3_symP [lemma, in MetaRocq.Utils.All_Forall]
Forall3_Forall2_right [lemma, in MetaRocq.Utils.All_Forall]
Forall3_Forall2_edges [lemma, in MetaRocq.Utils.All_Forall]
Forall3_Forall2_left [lemma, in MetaRocq.Utils.All_Forall]
Forall3_impl [lemma, in MetaRocq.Utils.All_Forall]
Forall3_All3 [lemma, in MetaRocq.Utils.All_Forall]
Forall3_sind [definition, in MetaRocq.Utils.All_Forall]
Forall3_ind [definition, in MetaRocq.Utils.All_Forall]
Forall3_cons [constructor, in MetaRocq.Utils.All_Forall]
Forall3_nil [constructor, in MetaRocq.Utils.All_Forall]
forget_inlining_info_transformation_ext' [lemma, in MetaRocq.Erasure.EInlining]
forget_inlining_info_transformation_ext [lemma, in MetaRocq.Erasure.EInlining]
forget_inlining_info_transformation [definition, in MetaRocq.Erasure.EInlining]
forget_inlining_info [definition, in MetaRocq.Erasure.EInlining]
forget_types [definition, in MetaRocq.Template.AstUtils]
forget_types_map_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
forget_types_map_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
forget_types_mapi_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
forget_types_fold_context_k [lemma, in MetaRocq.Common.BasicAst]
forget_types_length [lemma, in MetaRocq.Common.BasicAst]
forget_types [definition, in MetaRocq.Common.BasicAst]
forget_types_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
forget_types_map_context [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
forget_types_inst_case_context [lemma, in MetaRocq.PCUIC.PCUICCasesHelper]
form [inductive, in MetaRocq.Examples.tauto]
form_sind [definition, in MetaRocq.Examples.tauto]
form_rec [definition, in MetaRocq.Examples.tauto]
form_ind [definition, in MetaRocq.Examples.tauto]
form_rect [definition, in MetaRocq.Examples.tauto]
foron_free_vars_extended_subst [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
foroptb [definition, in MetaRocq.Utils.MROption]
foroptb_impl [lemma, in MetaRocq.Utils.MROption]
foroptb_proper_pointwise [instance, in MetaRocq.Utils.MROption]
foroptb_proper [instance, in MetaRocq.Utils.MROption]
foroptb2 [definition, in MetaRocq.Utils.MROption]
ForOption [inductive, in MetaRocq.Utils.MROption]
ForOption_sind [definition, in MetaRocq.Utils.MROption]
ForOption_ind [definition, in MetaRocq.Utils.MROption]
for_all_elements [lemma, in MetaRocq.Common.Universes]
fot_viewc [definition, in MetaRocq.Erasure.Typed.Erasure]
fot_view_sind [definition, in MetaRocq.Erasure.Typed.Erasure]
fot_view_rec [definition, in MetaRocq.Erasure.Typed.Erasure]
fot_view_ind [definition, in MetaRocq.Erasure.Typed.Erasure]
fot_view_rect [definition, in MetaRocq.Erasure.Typed.Erasure]
fot_view_other [constructor, in MetaRocq.Erasure.Typed.Erasure]
fot_view_sort [constructor, in MetaRocq.Erasure.Typed.Erasure]
fot_view_prod [constructor, in MetaRocq.Erasure.Typed.Erasure]
fot_view [inductive, in MetaRocq.Erasure.Typed.Erasure]
fo_v [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
fo_evalue_map [definition, in MetaRocq.ErasurePlugin.ErasureCorrectness]
fo_evalue [definition, in MetaRocq.ErasurePlugin.ErasureCorrectness]
fo_None [constructor, in MetaRocq.Utils.MROption]
fo_Some [constructor, in MetaRocq.Utils.MROption]
fresh [section, in MetaRocq.PCUIC.utils.PCUICPretty]
fresh [definition, in MetaRocq.Template.Checker]
fresh [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
freshnames [section, in MetaRocq.Erasure.EPretty]
freshnames.Σ [variable, in MetaRocq.Erasure.EPretty]
fresh_globals_cons_inv [lemma, in MetaRocq.Template.TemplateEnvMap]
fresh_global_map_on_snd [lemma, in MetaRocq.Erasure.EImplementBox]
fresh_globals_erase_global_decl_rec [lemma, in MetaRocq.Erasure.Typed.Extraction]
fresh_global_erase_global_decl_rec [lemma, in MetaRocq.Erasure.Typed.Extraction]
fresh_universe [definition, in MetaRocq.Common.Universes]
fresh_level [definition, in MetaRocq.Common.Universes]
fresh_names [definition, in MetaRocq.Template.Pretty]
fresh_name [definition, in MetaRocq.Template.Pretty]
fresh_id_from [definition, in MetaRocq.Template.Pretty]
fresh_global_In [lemma, in MetaRocq.Erasure.ErasureFunction]
fresh_globals_sind [definition, in MetaRocq.Erasure.Typed.ExAst]
fresh_globals_ind [definition, in MetaRocq.Erasure.Typed.ExAst]
fresh_globals_cons [constructor, in MetaRocq.Erasure.Typed.ExAst]
fresh_globals_empty [constructor, in MetaRocq.Erasure.Typed.ExAst]
fresh_globals [inductive, in MetaRocq.Erasure.Typed.ExAst]
fresh_global [definition, in MetaRocq.Erasure.Typed.ExAst]
fresh_global_app [lemma, in MetaRocq.PCUIC.PCUICFirstorder]
fresh_global_app [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
fresh_global_map [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
fresh_global_gen_transform_env [lemma, in MetaRocq.Erasure.EGenericGlobalMap]
fresh_global_subset [lemma, in MetaRocq.Erasure.EExtends]
fresh_names [definition, in MetaRocq.PCUIC.utils.PCUICPretty]
fresh_name [definition, in MetaRocq.PCUIC.utils.PCUICPretty]
fresh_id_from [definition, in MetaRocq.PCUIC.utils.PCUICPretty]
fresh_evar_id [definition, in MetaRocq.Common.BasicAst]
fresh_global_filter_deps [lemma, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
fresh_global_remove_match_on_box_env [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
fresh_global_gen_transform_env [lemma, in MetaRocq.Erasure.EGenericMapEnv]
fresh_global_trans [lemma, in MetaRocq.ErasurePlugin.ETransform]
fresh_subset [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
fresh_name [definition, in MetaRocq.Erasure.EPretty]
fresh_id_from [definition, in MetaRocq.Erasure.EPretty]
fresh_globals_cons_inv [lemma, in MetaRocq.Erasure.EEnvMap]
fresh_global [definition, in MetaRocq.Erasure.EGlobalEnv]
fresh_global_strip_env [lemma, in MetaRocq.Erasure.ERemoveParams]
fresh_global_trans_env [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
fresh.Σ [variable, in MetaRocq.PCUIC.utils.PCUICPretty]
from_oib [definition, in MetaRocq.Erasure.Typed.CertifyingEta]
FSets [module, in MetaRocq.Utils.MRFSets]
FSets.WFactsExtra_funSig [module, in MetaRocq.Utils.MRFSets]
FSets.WFactsExtra_fun.Equiv_alt_iff [lemma, in MetaRocq.Utils.MRFSets]
FSets.WFactsExtra_fun.Equiv_alt [definition, in MetaRocq.Utils.MRFSets]
FSets.WFactsExtra_fun.with_elt.elt [variable, in MetaRocq.Utils.MRFSets]
FSets.WFactsExtra_fun.with_elt [section, in MetaRocq.Utils.MRFSets]
FSets.WFactsExtra_fun [module, in MetaRocq.Utils.MRFSets]
FSets.WFacts_funSig [module, in MetaRocq.Utils.MRFSets]
fst_decompose_app_rec [lemma, in MetaRocq.Erasure.Prelim]
fst_decompose_app_rec [lemma, in MetaRocq.Erasure.EImplementBox]
fst_decompose_stack_nil [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
fst_ctx [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
fst_decompose_app_rec [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
fst_erase_pcuic_program' [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
fst_erase_pcuic_program [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
fst_decompose_app_rec [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
fst_pair [lemma, in MetaRocq.Utils.MRProd]
fst_eq [definition, in MetaRocq.Utils.MRProd]
fst' [projection, in MetaRocq.Examples.demo]
fuel [projection, in MetaRocq.Utils.MRUtils]
Fuel [record, in MetaRocq.Utils.MRUtils]
fuel [constructor, in MetaRocq.Utils.MRUtils]
Fuel [inductive, in MetaRocq.Utils.MRUtils]
full_subgraph_proper [instance, in MetaRocq.Common.uGraph]
Funtm [definition, in MetaRocq.Examples.demo]
Funtp [definition, in MetaRocq.Examples.demo]
Funtp2 [definition, in MetaRocq.Examples.demo]

---

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