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)

R (instance)

rebuild_wf_env_transform_pres_app [in MetaRocq.ErasurePlugin.ErasureCorrectness]
rebuild_wf_env_transform_pres_fo [in MetaRocq.ErasurePlugin.ErasureCorrectness]
rebuild_wf_env_extends' [in MetaRocq.ErasurePlugin.ETransform]
rebuild_wf_env_extends [in MetaRocq.ErasurePlugin.ETransform]
redp_red [in MetaRocq.SafeChecker.PCUICWfReduction]
redp_trans [in MetaRocq.SafeChecker.PCUICWfReduction]
red_ctx_alpha_refl [in MetaRocq.PCUIC.PCUICConfluence]
red_ctx_refl [in MetaRocq.PCUIC.PCUICConfluence]
red_Trans [in MetaRocq.PCUIC.PCUICConfluence]
red_Refl [in MetaRocq.PCUIC.PCUICConfluence]
red_terms_refl [in MetaRocq.PCUIC.PCUICConversion]
red_brs_refl [in MetaRocq.PCUIC.PCUICConversion]
red_brs_refl [in MetaRocq.SafeChecker.PCUICSafeConversion]
ReflectEq_term [in MetaRocq.Erasure.EReflect]
ReflectEq_of_listable [in MetaRocq.Utils.MRListable]
ReflectEq_EqDec [in MetaRocq.Utils.ReflectEq]
reflect_global_decl [in MetaRocq.Erasure.EReflect]
reflect_mutual_inductive_body [in MetaRocq.Erasure.EReflect]
reflect_one_inductive_body [in MetaRocq.Erasure.EReflect]
reflect_projection_body [in MetaRocq.Erasure.EReflect]
reflect_constructor_body [in MetaRocq.Erasure.EReflect]
reflect_constant_body [in MetaRocq.Erasure.EReflect]
reflect_stack [in MetaRocq.PCUIC.Syntax.PCUICPosition]
reflect_choice [in MetaRocq.PCUIC.Syntax.PCUICPosition]
reflect_Variance [in MetaRocq.Common.Reflect]
reflect_allowed_eliminations [in MetaRocq.Common.Reflect]
reflect_universes_decl [in MetaRocq.Common.Reflect]
reflect_ConstraintType [in MetaRocq.Common.Reflect]
reflect_recursivity_kind [in MetaRocq.Common.Reflect]
reflect_case_info [in MetaRocq.Common.Reflect]
reflect_cast_kind [in MetaRocq.Common.Reflect]
reflect_def [in MetaRocq.Common.Reflect]
reflect_aname [in MetaRocq.Common.Reflect]
reflect_relevance [in MetaRocq.Common.Reflect]
reflect_name [in MetaRocq.Common.Reflect]
reflect_levels [in MetaRocq.Common.Reflect]
reflect_prop_level [in MetaRocq.Common.Reflect]
reflect_prim_float [in MetaRocq.Common.Reflect]
reflect_prim_int [in MetaRocq.Common.Reflect]
reflect_global_decl [in MetaRocq.Template.ReflectAst]
reflect_mutual_inductive_body [in MetaRocq.Template.ReflectAst]
reflect_one_inductive_body [in MetaRocq.Template.ReflectAst]
reflect_projection_body [in MetaRocq.Template.ReflectAst]
reflect_constructor_body [in MetaRocq.Template.ReflectAst]
reflect_constant_body [in MetaRocq.Template.ReflectAst]
reflect_term [in MetaRocq.Template.ReflectAst]
reflect_eq_projection [in MetaRocq.Common.Kernames]
reflect_eq_inductive [in MetaRocq.Common.Kernames]
reflect_global_decl [in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflect_mutual_inductive_body [in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflect_one_inductive_body [in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflect_projection_body [in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflect_constructor_body [in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflect_constant_body [in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflect_eq_predicate [in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflect_prod [in MetaRocq.Utils.ReflectEq]
reflect_sig_true [in MetaRocq.Utils.ReflectEq]
reflect_bool [in MetaRocq.Utils.ReflectEq]
reflect_nat [in MetaRocq.Utils.ReflectEq]
reflect_list [in MetaRocq.Utils.ReflectEq]
reflect_option [in MetaRocq.Utils.ReflectEq]
reflect_eq_pstring [in MetaRocq.Erasure.EPrimitive]
reflect_eq_array [in MetaRocq.Erasure.EPrimitive]
reflect_eq_Z [in MetaRocq.Erasure.EPrimitive]
reflect_eq_pstring [in MetaRocq.PCUIC.utils.PCUICPrimitive]
reflect_eq_array [in MetaRocq.PCUIC.utils.PCUICPrimitive]
reflect_eq_spec_float [in MetaRocq.PCUIC.utils.PCUICPrimitive]
reflect_eq_uint63 [in MetaRocq.PCUIC.utils.PCUICPrimitive]
reflect_eq_Z [in MetaRocq.PCUIC.utils.PCUICPrimitive]
refl_eq_univ_prop [in MetaRocq.PCUIC.PCUICCumulProp]
relation_disjunction_Symmetric [in MetaRocq.Utils.MRRelations]
relation_disjunction_refl_r [in MetaRocq.Utils.MRRelations]
relation_disjunction_refl_l [in MetaRocq.Utils.MRRelations]
remove_params_optimization_pres_app [in MetaRocq.ErasurePlugin.ErasureCorrectness]
remove_params_optimization_pres [in MetaRocq.ErasurePlugin.ErasureCorrectness]
remove_match_on_box_pres_app [in MetaRocq.ErasurePlugin.ErasureCorrectness]
remove_match_on_box_pres [in MetaRocq.ErasurePlugin.ErasureCorrectness]
remove_match_on_box_extends' [in MetaRocq.ErasurePlugin.ETransform]
remove_match_on_box_extends [in MetaRocq.ErasurePlugin.ETransform]
remove_params_fast_extends' [in MetaRocq.ErasurePlugin.ETransform]
remove_params_fast_extends [in MetaRocq.ErasurePlugin.ETransform]
remove_params_extends' [in MetaRocq.ErasurePlugin.ETransform]
remove_params_extends [in MetaRocq.ErasurePlugin.ETransform]
rename_telescope_ext [in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_context_ext [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_branch_proper [in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_predicate_proper [in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_proper_pointwise [in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_proper [in MetaRocq.PCUIC.PCUICSigmaCalculus]
renaming_ext [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
ren_ext [in MetaRocq.PCUIC.PCUICSigmaCalculus]
reorder_cstrs_transformation_ext' [in MetaRocq.ErasurePlugin.ETransform]
reorder_cstrs_transformation_ext [in MetaRocq.ErasurePlugin.ETransform]
Req_refl [in MetaRocq.SafeChecker.PCUICSafeReduce]
Retroknowledge.extends_trans [in MetaRocq.Common.Environment]
Retroknowledge.extends_refl [in MetaRocq.Common.Environment]
Retroknowledge.reflect_t [in MetaRocq.Common.Environment]
rshiftk_proper [in MetaRocq.PCUIC.PCUICSigmaCalculus]

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)