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 (lemma)

validity [in MetaRocq.PCUIC.PCUICValidity]
validity_wf [in MetaRocq.PCUIC.PCUICSafeLemmata]
validity_env [in MetaRocq.PCUIC.PCUICValidity]
validity_wf_local [in MetaRocq.PCUIC.PCUICValidity]
valid_constraints_empty [in MetaRocq.PCUIC.PCUICEquality]
valid_config_impl [in MetaRocq.Common.Universes]
valid_subset [in MetaRocq.Common.Universes]
valid_cases_dearg_branch_body_rec [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_dearg_mask_branch_all_zeros [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_dearg_mask_branch_last_false [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_dearg_mask_branch_last_true [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_dearg_mask_dearg_aux [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_cases_dearg_lambdas [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_ind_mask_inductive [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_dearg_mask_constant [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_cases_constant [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_cases_cunfold_cofix [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_cases_cunfold_fix [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_cases_iota_red [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_cases_substl [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_cases_mkApps [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_cases_subst [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_cases_lift [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_case_masks_subst [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_dearg_branch_subst [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_case_masks_lift [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_cases_mkApps_inv [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_case_masks_dearg_branches [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_dearg_mask_branch_dearg [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_dearg_mask_dearg [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_dearg_mask_subst [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_dearg_mask_branch_lift [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_dearg_mask_lift [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_dearg_mask_csubst [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_dearg_mask_nil [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_dearg_mask_spec [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
valid_valid_gc [in MetaRocq.Common.uGraph]
valid_gc_constraints_aux [in MetaRocq.Common.uGraph]
valuation_labelling_eq [in MetaRocq.Common.uGraph]
values_final [in MetaRocq.Erasure.EWcbvEval]
value_final [in MetaRocq.Template.WcbvEval]
value_head_final [in MetaRocq.Template.WcbvEval]
value_head_spec [in MetaRocq.Template.WcbvEval]
value_mkApps_values [in MetaRocq.Template.WcbvEval]
value_mkApps_inv [in MetaRocq.Template.WcbvEval]
value_head_nApp [in MetaRocq.Template.WcbvEval]
value_values_ind [in MetaRocq.Template.WcbvEval]
value_mkApps_tFix [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
value_mkApps_inv' [in MetaRocq.PCUIC.PCUICProgress]
value_stuck_fix [in MetaRocq.PCUIC.PCUICProgress]
value_final [in MetaRocq.Erasure.EWcbvEval]
value_app_inv [in MetaRocq.Erasure.EWcbvEval]
value_head_spec' [in MetaRocq.Erasure.EWcbvEval]
value_head_final [in MetaRocq.Erasure.EWcbvEval]
value_head_spec [in MetaRocq.Erasure.EWcbvEval]
value_mkApps_values [in MetaRocq.Erasure.EWcbvEval]
value_mkApps_inv [in MetaRocq.Erasure.EWcbvEval]
value_head_nApp [in MetaRocq.Erasure.EWcbvEval]
value_values_ind [in MetaRocq.Erasure.EWcbvEval]
value_app [in MetaRocq.Erasure.EWcbvEval]
value_classification [in MetaRocq.PCUIC.PCUICClassification]
value_axiom_free [in MetaRocq.PCUIC.PCUICClassification]
value_whnf [in MetaRocq.PCUIC.PCUICClassification]
value_final [in MetaRocq.PCUIC.PCUICWcbvEval]
value_head_antimon [in MetaRocq.PCUIC.PCUICWcbvEval]
value_head_final [in MetaRocq.PCUIC.PCUICWcbvEval]
value_head_spec [in MetaRocq.PCUIC.PCUICWcbvEval]
value_mkApps_values [in MetaRocq.PCUIC.PCUICWcbvEval]
value_mkApps_inv [in MetaRocq.PCUIC.PCUICWcbvEval]
value_head_nApp [in MetaRocq.PCUIC.PCUICWcbvEval]
value_values_ind [in MetaRocq.PCUIC.PCUICWcbvEval]
value_app [in MetaRocq.PCUIC.PCUICWcbvEval]
value_trans [in MetaRocq.Erasure.ECoInductiveToInductive]
value_constructor_as_block [in MetaRocq.Erasure.ECoInductiveToInductive]
val_map_succ [in MetaRocq.Common.Universes]
val_succ [in MetaRocq.Common.Universes]
val_is_prop_false [in MetaRocq.Common.Universes]
val_is_sprop [in MetaRocq.Common.Universes]
val_is_prop [in MetaRocq.Common.Universes]
val_sort_sup [in MetaRocq.Common.Universes]
val_sup [in MetaRocq.Common.Universes]
val_add [in MetaRocq.Common.Universes]
val_caract [in MetaRocq.Common.Universes]
val_le_caract [in MetaRocq.Common.Universes]
val_ge_caract [in MetaRocq.Common.Universes]
val_In_max [in MetaRocq.Common.Universes]
val_In_le [in MetaRocq.Common.Universes]
val_fold_right [in MetaRocq.Common.Universes]
val_valuation_of_labelling2 [in MetaRocq.Common.uGraph]
val_ge_caract' [in MetaRocq.Common.uGraph]
val_le_caract' [in MetaRocq.Common.uGraph]
val_valuation_of_labelling [in MetaRocq.Common.uGraph]
val_valuation_of_labelling' [in MetaRocq.Common.uGraph]
val_labelling_of_valuation' [in MetaRocq.Common.uGraph]
val_labelling_of_valuation [in MetaRocq.Common.uGraph]
val_level_of_variable_level [in MetaRocq.Common.uGraph]
VariableLevel.compare_trans [in MetaRocq.Common.uGraph]
VariableLevel.compare_sym [in MetaRocq.Common.uGraph]
VariableLevel.compare_eq [in MetaRocq.Common.uGraph]
VariableLevel.compare_refl [in MetaRocq.Common.uGraph]
variance_universes_insts [in MetaRocq.PCUIC.PCUICInductiveInversion]
variance_universes_spec [in MetaRocq.SafeChecker.PCUICSafeChecker]
vasses_subst_context [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
vasses_app [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
verified_erasure_pipeline_theorem [in MetaRocq.ErasurePlugin.ErasureCorrectness]
verified_erasure_pipeline_firstorder_evalue_block [in MetaRocq.ErasurePlugin.ErasureCorrectness]
verified_erasure_pipeline_extends [in MetaRocq.ErasurePlugin.ErasureCorrectness]
verified_erasure_pipeline_lookup_env_in [in MetaRocq.ErasurePlugin.ErasureCorrectness]
verified_lambdabox_pipeline_mapping_extends' [in MetaRocq.ErasurePlugin.Erasure]
verified_lambdabox_pipeline_extends' [in MetaRocq.ErasurePlugin.Erasure]
view_lambda_fix_app_other [in MetaRocq.PCUIC.Syntax.PCUICViews]
view_fix_lambda [in MetaRocq.PCUIC.Syntax.PCUICViews]
view_lambda_fix_app_lambda_app [in MetaRocq.PCUIC.Syntax.PCUICViews]
view_lambda_fix_app_fix_app [in MetaRocq.PCUIC.Syntax.PCUICViews]
view_lambda_fix_app_lambda_app_sigma [in MetaRocq.PCUIC.Syntax.PCUICViews]
view_lambda_fix_app_fix_app_sigma [in MetaRocq.PCUIC.Syntax.PCUICViews]
view_lambda_fix_app [in MetaRocq.PCUIC.Syntax.PCUICViews]
v_t_spec [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