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

ECorrect.no [in MetaRocq.Erasure.Typed.ErasureCorrectness]
ECorrect.normalising_in [in MetaRocq.Erasure.Typed.ErasureCorrectness]
ECorrect.X [in MetaRocq.Erasure.Typed.ErasureCorrectness]
ECorrect.X_type [in MetaRocq.Erasure.Typed.ErasureCorrectness]
EEnvCorrect.normalising_in [in MetaRocq.Erasure.Typed.ErasureCorrectness]
EEnvCorrect.X [in MetaRocq.Erasure.Typed.ErasureCorrectness]
EEnvCorrect.X_type [in MetaRocq.Erasure.Typed.ErasureCorrectness]
EEnvFlags.efl [in MetaRocq.Erasure.EExtends]
EEnvFlags.efl [in MetaRocq.Erasure.EWellformed]
EEnvFlags.Σ [in MetaRocq.Erasure.EWellformed]
Elim'.cf [in MetaRocq.Erasure.EArities]
Elim'.Hcf [in MetaRocq.Erasure.EArities]
Elim'.wfΣ [in MetaRocq.Erasure.EArities]
Elim'.Σ [in MetaRocq.Erasure.EArities]
elim.ih [in MetaRocq.Erasure.ErasureFunctionProperties]
elim.P [in MetaRocq.Erasure.ErasureFunctionProperties]
elim.Σ [in MetaRocq.Erasure.ErasureFunctionProperties]
EnvCheck.abstract_structure [in MetaRocq.SafeChecker.PCUICErrors]
EnvMap.Poly.A [in MetaRocq.Common.EnvMap]
EnvTyping.All_local_env_size.ssize [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_size.csize [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_size.sorting [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_size.checking [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.Bidirectional.checking [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.Bidirectional.checking_size [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.Bidirectional.sorting [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.Bidirectional.sorting_size [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_size_gen.ssize [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_size_gen.csize [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_size_gen.sorting [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_size_gen.checking [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.Regular.typing [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.Regular.typing_size [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.TypeCtxInst.typing [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.TypeLocalOver.checking [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.TypeLocalOver.cproperty [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.TypeLocalOver.sorting [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.TypeLocalOver.sproperty [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.TypeLocal.typing [in MetaRocq.Common.EnvironmentTyping]
EqualityDecGen.cf [in MetaRocq.SafeChecker.PCUICEqualityDec]
EqualityDecGen.G [in MetaRocq.SafeChecker.PCUICEqualityDec]
EqualityDecGen.HG [in MetaRocq.SafeChecker.PCUICEqualityDec]
EqualityDecGen.hΣ [in MetaRocq.SafeChecker.PCUICEqualityDec]
EqualityDecGen.uctx [in MetaRocq.SafeChecker.PCUICEqualityDec]
EqualityDecGen.uctx' [in MetaRocq.SafeChecker.PCUICEqualityDec]
EqualityDecGen.Σ [in MetaRocq.SafeChecker.PCUICEqualityDec]
EqualityLemmas.cf [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
EqualityLemmas.wfΣ [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
EqualityLemmas.Σ [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
eq_list.eqA [in MetaRocq.Utils.ReflectEq]
eq_list.A [in MetaRocq.Utils.ReflectEq]
EraseEnv.fake_normalization [in MetaRocq.Erasure.Typed.Erasure]
EraseEnv.fake_guard_correct [in MetaRocq.Erasure.Typed.Erasure]
Erase.normalization_in [in MetaRocq.Erasure.ErasureFunction]
Erase.X [in MetaRocq.Erasure.ErasureFunction]
Erase.X_type [in MetaRocq.Erasure.ErasureFunction]
Eta.constants [in MetaRocq.Erasure.Typed.CertifyingEta]
Eta.ctors [in MetaRocq.Erasure.Typed.CertifyingEta]
Eta.Σ [in MetaRocq.Template.EtaExpand]
Eta.Σ [in MetaRocq.Erasure.Typed.CertifyingEta]
ETransformPresAppLam.Comp.env [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Comp.env' [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Comp.env'' [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Comp.eval [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Comp.eval' [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Comp.eval'' [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Comp.hpp [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Comp.is_etaexp'' [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Comp.is_etaexp' [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Comp.is_etaexp [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Comp.o [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Comp.oext [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Comp.o' [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Comp.o'ext [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Opt.env [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Opt.env' [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Opt.eval [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Opt.eval' [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Opt.is_etaexp' [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Opt.is_etaexp [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Opt.o [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.compile_fo_value' [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.compile_fo_value [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.env [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.env' [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.env'' [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.eval [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.eval' [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.eval'' [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.firstorder_value'' [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.firstorder_value' [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.firstorder_value [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.hpp [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.o [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.oext [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.o' [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.o'ext [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.ExtEq.env [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.ExtEq.env' [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.ExtEq.eval [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.ExtEq.eval' [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.ExtEq.firstorder_value' [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.ExtEq.firstorder_value [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.ExtEq.o [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Opt.compile_fo_value [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Opt.env [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Opt.env' [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Opt.eval [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Opt.eval' [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Opt.firstorder_value' [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Opt.firstorder_value [in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Opt.o [in MetaRocq.ErasurePlugin.ErasureCorrectness]
eval_mkApps_rect.IH [in MetaRocq.Erasure.EWcbvEvalInd]
eval_mkApps_rect.P [in MetaRocq.Erasure.EWcbvEvalInd]
eval_mkApps_rect.Σ [in MetaRocq.Erasure.EWcbvEvalInd]
eval_mkApps_rect.wfl [in MetaRocq.Erasure.EWcbvEvalInd]
eval_rect.P [in MetaRocq.Erasure.EWcbvEval]
eval_rect.Σ [in MetaRocq.Erasure.EWcbvEval]
eval_rect.wfl [in MetaRocq.Erasure.EWcbvEval]
expanded.Σ [in MetaRocq.Erasure.EEtaExpanded]
expanded.Σ [in MetaRocq.Template.EtaExpand]
expanded.Σ [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded.Σ [in MetaRocq.Erasure.EEtaExpandedFix]
ExtendsWf.cf [in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
ExtendsWf.cf [in MetaRocq.PCUIC.PCUICWeakeningEnv]
ExtendsWf.P [in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
ExtendsWf.P [in MetaRocq.PCUIC.PCUICWeakeningEnv]
ExtendsWf.Pcmp [in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
ExtendsWf.Pcmp [in MetaRocq.PCUIC.PCUICWeakeningEnv]
ExtendsWf.wf [in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
ExtendsWf.wf [in MetaRocq.PCUIC.PCUICWeakeningEnv]

---

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