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)

---

V

val [projection, in MetaRocq.Common.Universes]
val [constructor, in MetaRocq.Common.Universes]
Valid [constructor, in MetaRocq.Examples.tauto]
valid [definition, in MetaRocq.Examples.tauto]
validity [lemma, in MetaRocq.PCUIC.PCUICValidity]
Validity [section, in MetaRocq.PCUIC.PCUICValidity]
validity_wf [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
validity_term [abbreviation, in MetaRocq.PCUIC.PCUICValidity]
validity_env [lemma, in MetaRocq.PCUIC.PCUICValidity]
validity_wf_local [lemma, in MetaRocq.PCUIC.PCUICValidity]
Validity.cf [variable, in MetaRocq.PCUIC.PCUICValidity]
validpos [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
valid_subgoal [definition, in MetaRocq.Examples.tauto]
valid_constraints_empty [lemma, in MetaRocq.PCUIC.PCUICEquality]
valid_config_impl [lemma, in MetaRocq.Common.Universes]
valid_subset [lemma, in MetaRocq.Common.Universes]
valid_constraints [definition, in MetaRocq.Common.Universes]
valid_constraints0 [definition, in MetaRocq.Common.Universes]
valid_constraints0_dec [definition, in MetaRocq.Common.UniversesDec]
valid_constraints_dec [definition, in MetaRocq.Common.UniversesDec]
valid_masks_env [definition, in MetaRocq.Erasure.Typed.Optimize]
valid_masks_decl [definition, in MetaRocq.Erasure.Typed.Optimize]
valid_cases [definition, in MetaRocq.Erasure.Typed.Optimize]
valid_proj [definition, in MetaRocq.Erasure.Typed.Optimize]
valid_case_masks [definition, in MetaRocq.Erasure.Typed.Optimize]
valid_dearg_mask_branch [definition, in MetaRocq.Erasure.Typed.Optimize]
valid_dearg_mask [definition, in MetaRocq.Erasure.Typed.Optimize]
valid_cases_dearg_branch_body_rec [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_dearg_mask_branch_all_zeros [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_dearg_mask_branch_last_false [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_dearg_mask_branch_last_true [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_dearg_mask_dearg_aux [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_cases_dearg_lambdas [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_ind_mask_inductive [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_dearg_mask_constant [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_cases_constant [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_cases_cunfold_cofix [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_cases_cunfold_fix [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_cases_iota_red [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_cases_substl [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_cases_mkApps [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_cases_subst [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_cases_lift [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_case_masks_subst [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_dearg_branch_subst [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_case_masks_lift [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_cases_mkApps_inv [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_case_masks_dearg_branches [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_dearg_mask_branch_dearg [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_dearg_mask_dearg [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_dearg_mask_subst [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_dearg_mask_branch_lift [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_dearg_mask_lift [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_masks_env [abbreviation, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_masks_decl [abbreviation, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_cases [abbreviation, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_proj [abbreviation, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_case_masks [abbreviation, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_dearg_mask_csubst [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_dearg_mask_nil [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_dearg_mask_spec [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_valid_gc [lemma, in MetaRocq.Common.uGraph]
valid_gc_constraints_aux [lemma, in MetaRocq.Common.uGraph]
valid_gc_constraints_ext [definition, in MetaRocq.Common.uGraph]
valid_gc_constraints [definition, in MetaRocq.Common.uGraph]
valid_gc_constraint [definition, in MetaRocq.Common.uGraph]
valuation [record, in MetaRocq.Common.Universes]
valuation_poly [projection, in MetaRocq.Common.Universes]
valuation_mono [projection, in MetaRocq.Common.Universes]
valuation_labelling_eq [lemma, in MetaRocq.Common.uGraph]
valuation_of_labelling [definition, in MetaRocq.Common.uGraph]
value [inductive, in MetaRocq.Template.WcbvEval]
value [abbreviation, in MetaRocq.Erasure.EWcbvEval]
value [inductive, in MetaRocq.Erasure.EWcbvEval]
value [inductive, in MetaRocq.Erasure.EWcbvEvalNamed]
value [inductive, in MetaRocq.PCUIC.PCUICWcbvEval]
values_final [lemma, in MetaRocq.Erasure.EWcbvEval]
value_final [lemma, in MetaRocq.Template.WcbvEval]
value_head_final [lemma, in MetaRocq.Template.WcbvEval]
value_head_spec [lemma, in MetaRocq.Template.WcbvEval]
value_mkApps_values [lemma, in MetaRocq.Template.WcbvEval]
value_mkApps_inv [lemma, in MetaRocq.Template.WcbvEval]
value_head_nApp [lemma, in MetaRocq.Template.WcbvEval]
value_values_ind [lemma, in MetaRocq.Template.WcbvEval]
value_sind [definition, in MetaRocq.Template.WcbvEval]
value_rec [definition, in MetaRocq.Template.WcbvEval]
value_ind [definition, in MetaRocq.Template.WcbvEval]
value_rect [definition, in MetaRocq.Template.WcbvEval]
value_app [constructor, in MetaRocq.Template.WcbvEval]
value_atom [constructor, in MetaRocq.Template.WcbvEval]
value_head_fix [constructor, in MetaRocq.Template.WcbvEval]
value_head_ind [constructor, in MetaRocq.Template.WcbvEval]
value_head_cofix [constructor, in MetaRocq.Template.WcbvEval]
value_head_cstr [constructor, in MetaRocq.Template.WcbvEval]
value_head [inductive, in MetaRocq.Template.WcbvEval]
value_mkApps_tFix [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
value_mkApps_inv' [lemma, in MetaRocq.PCUIC.PCUICProgress]
value_stuck_fix [lemma, in MetaRocq.PCUIC.PCUICProgress]
value_final [lemma, in MetaRocq.Erasure.EWcbvEval]
value_app_inv [lemma, in MetaRocq.Erasure.EWcbvEval]
value_head_spec' [lemma, in MetaRocq.Erasure.EWcbvEval]
value_head_final [lemma, in MetaRocq.Erasure.EWcbvEval]
value_head_spec [lemma, in MetaRocq.Erasure.EWcbvEval]
value_mkApps_values [lemma, in MetaRocq.Erasure.EWcbvEval]
value_mkApps_inv [lemma, in MetaRocq.Erasure.EWcbvEval]
value_head_nApp [lemma, in MetaRocq.Erasure.EWcbvEval]
value_values_ind [lemma, in MetaRocq.Erasure.EWcbvEval]
value_app [lemma, in MetaRocq.Erasure.EWcbvEval]
value_head [abbreviation, in MetaRocq.Erasure.EWcbvEval]
value_app_nonnil [constructor, in MetaRocq.Erasure.EWcbvEval]
value_constructor [constructor, in MetaRocq.Erasure.EWcbvEval]
value_atom [constructor, in MetaRocq.Erasure.EWcbvEval]
value_head_fix [constructor, in MetaRocq.Erasure.EWcbvEval]
value_head_cofix [constructor, in MetaRocq.Erasure.EWcbvEval]
value_head_cstr [constructor, in MetaRocq.Erasure.EWcbvEval]
value_head [inductive, in MetaRocq.Erasure.EWcbvEval]
value_sind [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
value_rec [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
value_ind [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
value_rect [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
value_classification [lemma, in MetaRocq.PCUIC.PCUICClassification]
value_axiom_free [lemma, in MetaRocq.PCUIC.PCUICClassification]
value_whnf [lemma, in MetaRocq.PCUIC.PCUICClassification]
value_final [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
value_head_antimon [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
value_head_final [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
value_head_spec [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
value_mkApps_values [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
value_mkApps_inv [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
value_head_nApp [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
value_values_ind [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
value_app [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
value_sind [definition, in MetaRocq.PCUIC.PCUICWcbvEval]
value_rec [definition, in MetaRocq.PCUIC.PCUICWcbvEval]
value_ind [definition, in MetaRocq.PCUIC.PCUICWcbvEval]
value_rect [definition, in MetaRocq.PCUIC.PCUICWcbvEval]
value_app_nonnil [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
value_atomic [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
value_head_fix [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
value_head_cofix [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
value_head_ind [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
value_head_cstr [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
value_head [inductive, in MetaRocq.PCUIC.PCUICWcbvEval]
value_trans [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
value_constructor_as_block [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
val_map_succ [lemma, in MetaRocq.Common.Universes]
val_succ [lemma, in MetaRocq.Common.Universes]
val_is_prop_false [lemma, in MetaRocq.Common.Universes]
val_is_sprop [lemma, in MetaRocq.Common.Universes]
val_is_prop [lemma, in MetaRocq.Common.Universes]
val_sort_sup [lemma, in MetaRocq.Common.Universes]
val_sup [lemma, in MetaRocq.Common.Universes]
val_add [lemma, in MetaRocq.Common.Universes]
val_caract [lemma, in MetaRocq.Common.Universes]
val_le_caract [lemma, in MetaRocq.Common.Universes]
val_ge_caract [lemma, in MetaRocq.Common.Universes]
val_In_max [lemma, in MetaRocq.Common.Universes]
val_In_le [lemma, in MetaRocq.Common.Universes]
val_fold_right [lemma, in MetaRocq.Common.Universes]
val_valuation_of_labelling2 [lemma, in MetaRocq.Common.uGraph]
val_ge_caract' [lemma, in MetaRocq.Common.uGraph]
val_le_caract' [lemma, in MetaRocq.Common.uGraph]
val_valuation_of_labelling [lemma, in MetaRocq.Common.uGraph]
val_valuation_of_labelling' [lemma, in MetaRocq.Common.uGraph]
val_labelling_of_valuation' [lemma, in MetaRocq.Common.uGraph]
val_labelling_of_valuation [lemma, in MetaRocq.Common.uGraph]
val_level_of_variable_level [lemma, in MetaRocq.Common.uGraph]
Var [constructor, in MetaRocq.Examples.tauto]
var [definition, in MetaRocq.Examples.tauto]
var [constructor, in MetaRocq.Examples.add_constructor]
VariableLevel [module, in MetaRocq.Common.uGraph]
VariableLevelOT [module, in MetaRocq.Common.uGraph]
VariableLevel.compare [definition, in MetaRocq.Common.uGraph]
VariableLevel.compare_trans [lemma, in MetaRocq.Common.uGraph]
VariableLevel.compare_sym [lemma, in MetaRocq.Common.uGraph]
VariableLevel.compare_eq [lemma, in MetaRocq.Common.uGraph]
VariableLevel.compare_refl [lemma, in MetaRocq.Common.uGraph]
VariableLevel.compare_spec [definition, in MetaRocq.Common.uGraph]
VariableLevel.eq_dec [definition, in MetaRocq.Common.uGraph]
VariableLevel.Evaluable [instance, in MetaRocq.Common.uGraph]
VariableLevel.level [constructor, in MetaRocq.Common.uGraph]
VariableLevel.lt [definition, in MetaRocq.Common.uGraph]
VariableLevel.lt_compat [definition, in MetaRocq.Common.uGraph]
VariableLevel.lt_trans [definition, in MetaRocq.Common.uGraph]
VariableLevel.lt_strorder [instance, in MetaRocq.Common.uGraph]
VariableLevel.lvar [constructor, in MetaRocq.Common.uGraph]
VariableLevel.t [definition, in MetaRocq.Common.uGraph]
VariableLevel.to_level [definition, in MetaRocq.Common.uGraph]
VariableLevel.to_noprop [definition, in MetaRocq.Common.uGraph]
VariableLevel.t__sind [definition, in MetaRocq.Common.uGraph]
VariableLevel.t__rec [definition, in MetaRocq.Common.uGraph]
VariableLevel.t__ind [definition, in MetaRocq.Common.uGraph]
VariableLevel.t__rect [definition, in MetaRocq.Common.uGraph]
VariableLevel.t_ [inductive, in MetaRocq.Common.uGraph]
_ ?= _ (var_level) [notation, in MetaRocq.Common.uGraph]
variable_of_level [definition, in MetaRocq.Common.uGraph]
Variance [constructor, in MetaRocq.Common.Universes]
Variance [module, in MetaRocq.Common.Universes]
variance_universes_insts [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
variance_universes_spec [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
Variance.Covariant [constructor, in MetaRocq.Common.Universes]
Variance.Invariant [constructor, in MetaRocq.Common.Universes]
Variance.Irrelevant [constructor, in MetaRocq.Common.Universes]
Variance.t [inductive, in MetaRocq.Common.Universes]
Variance.t_sind [definition, in MetaRocq.Common.Universes]
Variance.t_rec [definition, in MetaRocq.Common.Universes]
Variance.t_ind [definition, in MetaRocq.Common.Universes]
Variance.t_rect [definition, in MetaRocq.Common.Universes]
VarRef [constructor, in MetaRocq.Common.Kernames]
vass [definition, in MetaRocq.Erasure.EAst]
vasses [definition, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
vasses_subst_context [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
vasses_app [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
vass_open_decl [definition, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
vClos [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
vConstruct [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
vdef [definition, in MetaRocq.Erasure.EAst]
vec_repeat [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
verified_erasure_pipeline_theorem [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
verified_erasure_pipeline_firstorder_evalue_block [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
verified_erasure_pipeline_extends [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
verified_erasure_pipeline_lookup_env_in [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
verified_typed_erasure_pipeline [definition, in MetaRocq.ErasurePlugin.Erasure]
verified_lambdabox_typed_pipeline [definition, in MetaRocq.ErasurePlugin.Erasure]
verified_lambdabox_pipeline_mapping_extends' [lemma, in MetaRocq.ErasurePlugin.Erasure]
verified_lambdabox_pipeline_extends' [lemma, in MetaRocq.ErasurePlugin.Erasure]
verified_lambdabox_pipeline_mapping_extends [instance, in MetaRocq.ErasurePlugin.Erasure]
verified_lambdabox_pipeline_extends [instance, in MetaRocq.ErasurePlugin.Erasure]
verified_erasure_pipeline_mapping [definition, in MetaRocq.ErasurePlugin.Erasure]
verified_erasure_pipeline [definition, in MetaRocq.ErasurePlugin.Erasure]
verified_lambdabox_pipeline_mapping [definition, in MetaRocq.ErasurePlugin.Erasure]
verified_lambdabox_pipeline [definition, in MetaRocq.ErasurePlugin.Erasure]
view_prodc [definition, in MetaRocq.Erasure.Typed.Erasure]
view_prod_sind [definition, in MetaRocq.Erasure.Typed.Erasure]
view_prod_rec [definition, in MetaRocq.Erasure.Typed.Erasure]
view_prod_ind [definition, in MetaRocq.Erasure.Typed.Erasure]
view_prod_rect [definition, in MetaRocq.Erasure.Typed.Erasure]
view_prod_other [constructor, in MetaRocq.Erasure.Typed.Erasure]
view_prod_prod [constructor, in MetaRocq.Erasure.Typed.Erasure]
view_prod [inductive, in MetaRocq.Erasure.Typed.Erasure]
view_other [constructor, in MetaRocq.SafeChecker.PCUICSafeReduce]
view_construct [constructor, in MetaRocq.SafeChecker.PCUICSafeReduce]
view_prod_sortc [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_prod_sort_sind [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_prod_sort_rec [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_prod_sort_ind [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_prod_sort_rect [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_prod_sort_other [constructor, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_prod_sort_sort [constructor, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_prod_sort_prod [constructor, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_prod_sort [inductive, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_indc [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_ind_sind [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_ind_rec [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_ind_ind [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_ind_rect [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_ind_other [constructor, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_ind_tInd [constructor, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_ind [inductive, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_prodc [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_prod_sind [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_prod_rec [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_prod_ind [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_prod_rect [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_prod_other [constructor, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_prod_prod [constructor, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_prod [inductive, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_sortc [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_sort_sind [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_sort_rec [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_sort_ind [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_sort_rect [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_sort_other [constructor, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_sort_sort [constructor, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_sort [inductive, in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_other [constructor, in MetaRocq.Erasure.EEtaExpanded]
view_construct [constructor, in MetaRocq.Erasure.EEtaExpanded]
view_lambda_fix_app_other [lemma, in MetaRocq.PCUIC.Syntax.PCUICViews]
view_fix_lambda [lemma, in MetaRocq.PCUIC.Syntax.PCUICViews]
view_construct0_cofix [definition, in MetaRocq.PCUIC.Syntax.PCUICViews]
view_construct_cofix [definition, in MetaRocq.PCUIC.Syntax.PCUICViews]
view_lambda_fix_app_lambda_app [lemma, in MetaRocq.PCUIC.Syntax.PCUICViews]
view_lambda_fix_app_fix_app [lemma, in MetaRocq.PCUIC.Syntax.PCUICViews]
view_lambda_fix_app_lambda_app_sigma [lemma, in MetaRocq.PCUIC.Syntax.PCUICViews]
view_lambda_fix_app_fix_app_sigma [lemma, in MetaRocq.PCUIC.Syntax.PCUICViews]
view_lambda_fix_app [lemma, in MetaRocq.PCUIC.Syntax.PCUICViews]
vLazy [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
VmCast [constructor, in MetaRocq.Common.BasicAst]
vPrim [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
vRecClos [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
VSet [module, in MetaRocq.Common.uGraph]
vtn [abbreviation, in MetaRocq.Common.uGraph]
v_t_spec [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]

---

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