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)

---

E (instance)

Empty_set_FinitelyListablePackage [in MetaRocq.Utils.MRListable]
envcheck_monad_exc [in MetaRocq.SafeChecker.PCUICErrors]
envcheck_monad [in MetaRocq.SafeChecker.PCUICErrors]
envcheck_monad [in MetaRocq.Template.Checker]
EnvDecide.constant_body_eq_dec [in MetaRocq.Template.ReflectAst]
EnvDecide.constructor_body_eq_dec [in MetaRocq.Template.ReflectAst]
EnvDecide.context_eq_dec [in MetaRocq.Template.ReflectAst]
EnvDecide.global_decl_eq_dec [in MetaRocq.Template.ReflectAst]
EnvDecide.mutual_inductive_body_eq_dec [in MetaRocq.Template.ReflectAst]
EnvDecide.one_inductive_body_eq_dec [in MetaRocq.Template.ReflectAst]
EnvDecide.projection_body_eq_dec [in MetaRocq.Template.ReflectAst]
EnvironmentDecide.constant_body_eq_dec [in MetaRocq.Common.Environment]
EnvironmentDecide.constructor_body_eq_dec [in MetaRocq.Common.Environment]
EnvironmentDecide.context_eq_dec [in MetaRocq.Common.Environment]
EnvironmentDecide.global_decl_eq_dec [in MetaRocq.Common.Environment]
EnvironmentDecide.mutual_inductive_body_eq_dec [in MetaRocq.Common.Environment]
EnvironmentDecide.one_inductive_body_eq_dec [in MetaRocq.Common.Environment]
EnvironmentDecide.projection_body_eq_dec [in MetaRocq.Common.Environment]
Environment.extends_trans [in MetaRocq.Common.Environment]
Environment.extends_strictly_on_decls_trans [in MetaRocq.Common.Environment]
Environment.extends_decls_trans [in MetaRocq.Common.Environment]
Environment.extends_decls_refl [in MetaRocq.Common.Environment]
Environment.extends_strictly_on_decls_extends_subrel [in MetaRocq.Common.Environment]
Environment.extends_decls_extends_subrel [in MetaRocq.Common.Environment]
Environment.extends_strictly_on_decls_extends [in MetaRocq.Common.Environment]
Environment.extends_decls_extends [in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_trans [in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_refl [in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_extends_subrel [in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_extends_strictly_on_decls_subrel [in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_extends_decls_subrel [in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_extends_strictly_on_decls [in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_extends_decls [in MetaRocq.Common.Environment]
Environment.subst_instance_context [in MetaRocq.Common.Environment]
Environment.subst_instance_decl [in MetaRocq.Common.Environment]
eqbrs_refl [in MetaRocq.PCUIC.PCUICConversion]
eqb_ctx [in MetaRocq.Template.ReflectAst]
eqb_ctx [in MetaRocq.PCUIC.Syntax.PCUICReflect]
eqb_term_reflect [in MetaRocq.PCUIC.Syntax.PCUICReflect]
EqDec_term [in MetaRocq.Erasure.EReflect]
EqDec_stack_entry [in MetaRocq.PCUIC.Syntax.PCUICPosition]
EqDec_branch_hole [in MetaRocq.PCUIC.Syntax.PCUICPosition]
EqDec_predicate_hole [in MetaRocq.PCUIC.Syntax.PCUICPosition]
EqDec_context_decl_hole [in MetaRocq.PCUIC.Syntax.PCUICPosition]
EqDec_def_hole [in MetaRocq.PCUIC.Syntax.PCUICPosition]
eqdec_binder_annot [in MetaRocq.Common.BasicAst]
EqDec_term [in MetaRocq.Template.ReflectAst]
EqDec_pstring [in MetaRocq.Template.ReflectAst]
EqDec_term [in MetaRocq.PCUIC.Syntax.PCUICReflect]
eqt_refl [in MetaRocq.SafeChecker.PCUICSafeConversion]
equal_graph_equiv [in MetaRocq.Common.uGraph]
equiv_True [in MetaRocq.PCUIC.PCUICCumulProp]
equiv_eq_univ_prop [in MetaRocq.PCUIC.PCUICCumulProp]
eq_term_leq_term [in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_leq [in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_empty_impl [in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_impl [in MetaRocq.PCUIC.PCUICEquality]
eq_term_equiv [in MetaRocq.PCUIC.PCUICEquality]
eq_context_equiv [in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_equiv [in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_trans [in MetaRocq.PCUIC.PCUICEquality]
eq_predicate_trans [in MetaRocq.PCUIC.PCUICEquality]
eq_predicate_sym [in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_sym [in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_refl [in MetaRocq.PCUIC.PCUICEquality]
eq_mfixpoint_refl [in MetaRocq.PCUIC.PCUICEquality]
eq_branches_refl [in MetaRocq.PCUIC.PCUICEquality]
eq_predicate_refl [in MetaRocq.PCUIC.PCUICEquality]
eq_binder_annot_equiv [in MetaRocq.PCUIC.PCUICEquality]
eq_context_trans [in MetaRocq.PCUIC.PCUICEquality]
eq_context_sym [in MetaRocq.PCUIC.PCUICEquality]
eq_context_refl [in MetaRocq.PCUIC.PCUICEquality]
eq_decl_upto_names_trans [in MetaRocq.PCUIC.PCUICEquality]
eq_decl_upto_names_sym [in MetaRocq.PCUIC.PCUICEquality]
eq_decl_upto_names_refl [in MetaRocq.PCUIC.PCUICEquality]
eq_sort_equivalence [in MetaRocq.Common.Universes]
eq_leq_sort [in MetaRocq.Common.Universes]
eq_sort_trans [in MetaRocq.Common.Universes]
eq_sort_sym [in MetaRocq.Common.Universes]
eq_sort_refl [in MetaRocq.Common.Universes]
eq_universe_equivalence [in MetaRocq.Common.Universes]
eq_leq_universe [in MetaRocq.Common.Universes]
eq_universe_trans [in MetaRocq.Common.Universes]
eq_universe_sym [in MetaRocq.Common.Universes]
eq_universe_refl [in MetaRocq.Common.Universes]
eq_term_upto_univ_weaken_env [in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
eq_term_upto_univ_impl [in MetaRocq.Template.TermEquality]
eq_binder_annots_refl [in MetaRocq.Template.TermEquality]
eq_binder_annot_equiv [in MetaRocq.Template.TermEquality]
eq_decl_reflect [in MetaRocq.Common.Reflect]
eq_subrel_eq_sort [in MetaRocq.PCUIC.PCUICContextConversion]
eq_subrel_eq_univ [in MetaRocq.PCUIC.PCUICContextConversion]
eq_context_upto_univ_subst_preserved [in MetaRocq.PCUIC.PCUICConfluence]
eq_predicate [in MetaRocq.Template.ReflectAst]
eq_context_upto_subst_preserved [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
eq_term_upto_univ_subst_preserved [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
eq_sort_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
eq_universe_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
eq_universe_SubstUnivPreserving [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
eq_ctx [in MetaRocq.PCUIC.Syntax.PCUICReflect]
ETransformPresAppLam.compose [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.compose [in MetaRocq.ErasurePlugin.ErasureCorrectness]
extraction_checker_flags [in MetaRocq.Common.config]
extraction_normalizing [in MetaRocq.PCUIC.PCUICSN]

---

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