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)

C (instance)

canonical_abstract_env_prop [in MetaRocq.SafeChecker.PCUICWfEnvImpl]
canonical_abstract_env_struct [in MetaRocq.SafeChecker.PCUICWfEnvImpl]
closedP_proper [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
closed_red_trans [in MetaRocq.PCUIC.PCUICContextConversion]
clos_refl_trans_ctx_t_trans [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_t_refl [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_trans [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_refl [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_sym_trans_Transitive [in MetaRocq.Utils.MRRelations]
clos_refl_sym_trans_Reflexive [in MetaRocq.Utils.MRRelations]
clos_refl_sym_trans_Symmetric [in MetaRocq.Utils.MRRelations]
clos_sym_Symmetric [in MetaRocq.Utils.MRRelations]
clos_rt_trans_Symmetric [in MetaRocq.Utils.MRRelations]
clos_rt_refl [in MetaRocq.Utils.MRRelations]
clos_rt_trans [in MetaRocq.Utils.MRRelations]
cmp_global_instance_empty_impl [in MetaRocq.PCUIC.PCUICEquality]
cmp_global_instance_impl [in MetaRocq.PCUIC.PCUICEquality]
cmp_global_instance_impl_same_napp [in MetaRocq.PCUIC.PCUICEquality]
cmp_global_instance_antisym [in MetaRocq.PCUIC.PCUICEquality]
cmp_global_instance_equiv [in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_equiv [in MetaRocq.PCUIC.PCUICEquality]
cmp_global_instance_trans [in MetaRocq.PCUIC.PCUICEquality]
cmp_global_instance_sym [in MetaRocq.PCUIC.PCUICEquality]
cmp_global_instance_refl [in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_variance_trans [in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_variance_sym [in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_variance_trans [in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_variance_sym [in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_trans [in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_sym [in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_refl [in MetaRocq.PCUIC.PCUICEquality]
cmp_global_instance_impl [in MetaRocq.Template.TermEquality]
cmp_global_instance_impl_same_napp [in MetaRocq.Template.TermEquality]
coinductive_to_inductive_transformation_ext' [in MetaRocq.ErasurePlugin.ETransform]
coinductive_to_inductive_transformation_ext [in MetaRocq.ErasurePlugin.ETransform]
compare_term_trans [in MetaRocq.PCUIC.PCUICEquality]
compare_term_sym [in MetaRocq.PCUIC.PCUICEquality]
compare_term_refl [in MetaRocq.PCUIC.PCUICEquality]
compare_decl_trans [in MetaRocq.PCUIC.PCUICEquality]
compare_decl_sym [in MetaRocq.PCUIC.PCUICEquality]
compare_decl_refl [in MetaRocq.PCUIC.PCUICEquality]
compare_sort_preorder [in MetaRocq.Common.Universes]
compare_sort_trans [in MetaRocq.Common.Universes]
compare_sort_refl [in MetaRocq.Common.Universes]
compare_sort_subrel [in MetaRocq.Common.Universes]
compare_universe_preorder [in MetaRocq.Common.Universes]
compare_universe_trans [in MetaRocq.Common.Universes]
compare_universe_refl [in MetaRocq.Common.Universes]
compare_universe_subrel [in MetaRocq.Common.Universes]
compare_context_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
compare_decl_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
compare_decls_subst_preserved [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
compare_sort_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
compare_universe_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
compare_sort_substu [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
compare_universe_substu [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
compare_decls_refl [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
confluent_proper [in MetaRocq.PCUIC.PCUICConfluence]
consistent_proper [in MetaRocq.SafeChecker.PCUICWfEnv]
consistent_no_loop [in MetaRocq.Common.uGraph]
ConstraintSetsUIP.cs_tree_reflect [in MetaRocq.Common.Reflect]
ConstraintSetsUIP.reflect_ConstraintSet [in MetaRocq.Common.Reflect]
ConstraintType.lt_compat [in MetaRocq.Common.Universes]
ConstraintType.lt_strorder [in MetaRocq.Common.Universes]
constructors_as_blocks_transformation_pres_app [in MetaRocq.ErasurePlugin.ErasureCorrectness]
constructors_as_blocks_transformation_pres [in MetaRocq.ErasurePlugin.ErasureCorrectness]
constructors_as_blocks_extends' [in MetaRocq.ErasurePlugin.ETransform]
constructors_as_blocks_extends [in MetaRocq.ErasurePlugin.ETransform]
context_reflect [in MetaRocq.PCUIC.PCUICAst]
conv_ctx_refl [in MetaRocq.PCUIC.PCUICCumulativity]
conv_sym [in MetaRocq.PCUIC.PCUICCumulativity]
conv_refl' [in MetaRocq.PCUIC.PCUICCumulativity]
conv_decls_refl [in MetaRocq.PCUIC.PCUICCumulativity]
conv_context_refl [in MetaRocq.PCUIC.PCUICSR]
conv_trans [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
conv_context_sym [in MetaRocq.PCUIC.PCUICContextConversion]
conv_ctx_refl [in MetaRocq.PCUIC.PCUICCumulativitySpec]
conv_decls_refl [in MetaRocq.PCUIC.PCUICCumulativitySpec]
conv_refl' [in MetaRocq.PCUIC.PCUICCumulativitySpec]
conv_cum_trans [in MetaRocq.SafeChecker.PCUICSafeConversion]
cored_transitive [in MetaRocq.SafeChecker.PCUICWfReduction]
correct_labelling_proper [in MetaRocq.Common.uGraph]
creflexive_eq [in MetaRocq.PCUIC.PCUICEquality]
CS_For_all_proper [in MetaRocq.Common.Universes]
cumul_ctx_refl [in MetaRocq.PCUIC.PCUICCumulativity]
cumul_refl' [in MetaRocq.PCUIC.PCUICCumulativity]
cumul_decls_refl [in MetaRocq.PCUIC.PCUICCumulativity]
cumul_pb_decls_refl [in MetaRocq.PCUIC.PCUICCumulativity]
cumul_trans [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
cumul_ctx_refl [in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_pb_ctx_refl [in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_decls_refl [in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_pb_decls_refl [in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_spec_refl [in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_prop_sym' [in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_transitive [in MetaRocq.PCUIC.PCUICCumulProp]

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)