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

CaseBranchTypeBeta.cf [in MetaRocq.PCUIC.PCUICCasesHelper]
CaseDefinitions.cf [in MetaRocq.PCUIC.PCUICCasesHelper]
CaseDefinitions.ind [in MetaRocq.PCUIC.PCUICCasesHelper]
CaseDefinitions.mib [in MetaRocq.PCUIC.PCUICCasesHelper]
CaseDefinitions.oib [in MetaRocq.PCUIC.PCUICCasesHelper]
CaseDefinitions.pparams [in MetaRocq.PCUIC.PCUICCasesHelper]
CaseDefinitions.puinst [in MetaRocq.PCUIC.PCUICCasesHelper]
cf.cf [in MetaRocq.PCUIC.PCUICFirstorder]
CheckEnv.cf [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadAllAll.A [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadAllAll.AA [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadAllAll.BB [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadAllAll.f [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadAllAll.M [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadAllAll.P [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadAllAll.Q [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadAllAll.T [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadLiftExt.ext [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadLiftExt.M [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadLiftExt.P [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadLiftExt.T [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadLiftExt.X [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadLiftExt.XX_ext' [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadLiftExt.XX_ext [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadLiftExt.X_ext [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadMapi.A [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadMapi.B [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadMapi.f [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadMapi.M [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadMapi.T [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.monad_Alli_nth_forall.P [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.monad_Alli_nth_forall.A [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.monad_Alli_nth_forall.M [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.monad_Alli_nth_forall.T [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.monad_Alli_nth_forall.BB [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.monad_Alli_nth_forall.AA [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.nor [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.PositivityCheck.normalization_in [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.PositivityCheck.X_ext [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.X_impl [in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckerFlags.cf [in MetaRocq.PCUIC.PCUICWfUniverses]
CheckerFlags.WfUniverses.Σ [in MetaRocq.PCUIC.PCUICWfUniverses]
Checker.cf [in MetaRocq.Template.Checker]
Checker.F [in MetaRocq.Template.Checker]
CheckLeqProcedure.cf [in MetaRocq.Common.uGraph]
CheckLeqProcedure.leqb_level_n [in MetaRocq.Common.uGraph]
CheckLeq.cf [in MetaRocq.Common.uGraph]
CheckLeq.G [in MetaRocq.Common.uGraph]
CheckLeq.HC [in MetaRocq.Common.uGraph]
CheckLeq.HG [in MetaRocq.Common.uGraph]
CheckLeq.Huctx [in MetaRocq.Common.uGraph]
CheckLeq.levels_declared_sort [in MetaRocq.Common.uGraph]
CheckLeq.uctx [in MetaRocq.Common.uGraph]
CheckLeq2.cf [in MetaRocq.Common.uGraph]
CheckLeq2.expr_declared [in MetaRocq.Common.uGraph]
CheckLeq2.G [in MetaRocq.Common.uGraph]
CheckLeq2.HC [in MetaRocq.Common.uGraph]
CheckLeq2.HC' [in MetaRocq.Common.uGraph]
CheckLeq2.HG [in MetaRocq.Common.uGraph]
CheckLeq2.HG' [in MetaRocq.Common.uGraph]
CheckLeq2.Huctx [in MetaRocq.Common.uGraph]
CheckLeq2.Huctx' [in MetaRocq.Common.uGraph]
CheckLeq2.levels_declared_sort [in MetaRocq.Common.uGraph]
CheckLeq2.levels_declared [in MetaRocq.Common.uGraph]
CheckLeq2.level_declared [in MetaRocq.Common.uGraph]
CheckLeq2.uctx [in MetaRocq.Common.uGraph]
classification.cf [in MetaRocq.PCUIC.PCUICClassification]
classification.wfΣ [in MetaRocq.PCUIC.PCUICClassification]
classification.Σ [in MetaRocq.PCUIC.PCUICClassification]
ClosedSpineSubst.cf [in MetaRocq.PCUIC.PCUICSpine]
Closedu.k [in MetaRocq.Common.Universes]
ConfluenceFacts.cf [in MetaRocq.PCUIC.PCUICConfluence]
ConfluenceFacts.wfΣ [in MetaRocq.PCUIC.PCUICConfluence]
ConfluenceFacts.Σ [in MetaRocq.PCUIC.PCUICConfluence]
ContextChangeTypesReduction.cf [in MetaRocq.PCUIC.PCUICRedTypeIrrelevance]
ContextChangeTypesReduction.Σ [in MetaRocq.PCUIC.PCUICRedTypeIrrelevance]
ContextConversion.cf [in MetaRocq.PCUIC.PCUICCumulativity]
ContextConversion.cf [in MetaRocq.PCUIC.PCUICContextConversion]
ContextConversion.cf [in MetaRocq.PCUIC.PCUICCumulativitySpec]
ContextConversion.wfΣ [in MetaRocq.PCUIC.PCUICContextConversion]
ContextConversion.Σ [in MetaRocq.PCUIC.PCUICCumulativity]
ContextConversion.Σ [in MetaRocq.PCUIC.PCUICContextConversion]
ContextConversion.Σ [in MetaRocq.PCUIC.PCUICCumulativitySpec]
ContextMap.f [in MetaRocq.Common.BasicAst]
ContextMap.term [in MetaRocq.Common.BasicAst]
ContextMap.term' [in MetaRocq.Common.BasicAst]
ContextReduction.cf [in MetaRocq.PCUIC.PCUICContextConversion]
ContextReduction.wfΣ [in MetaRocq.PCUIC.PCUICContextConversion]
ContextReduction.Σ [in MetaRocq.PCUIC.PCUICContextConversion]
Contexts.term [in MetaRocq.Common.BasicAst]
Contexts.term [in MetaRocq.Common.BasicAst]
Contexts.term [in MetaRocq.Common.BasicAst]
Contexts.term' [in MetaRocq.Common.BasicAst]
Contexts.term' [in MetaRocq.Common.BasicAst]
Contexts.term'' [in MetaRocq.Common.BasicAst]
Contexts.term'' [in MetaRocq.Common.BasicAst]
ContextTestK.f [in MetaRocq.Common.BasicAst]
ContextTestK.k [in MetaRocq.Common.BasicAst]
ContextTestK.term [in MetaRocq.Common.BasicAst]
ContextTest.f [in MetaRocq.Common.BasicAst]
ContextTest.term [in MetaRocq.Common.BasicAst]
ConvCongruences.cf [in MetaRocq.PCUIC.PCUICConversion]
ConvCongruences.wfΣ [in MetaRocq.PCUIC.PCUICConversion]
ConvCongruences.Σ [in MetaRocq.PCUIC.PCUICConversion]
Conversion.cf [in MetaRocq.SafeChecker.PCUICSafeConversion]
Conversion.Conversion.cumul_gen [in MetaRocq.Common.EnvironmentTyping]
Conversion.flags [in MetaRocq.Template.Checker]
Conversion.G [in MetaRocq.Template.Checker]
Conversion.nor [in MetaRocq.SafeChecker.PCUICSafeConversion]
Conversion.normalization_in [in MetaRocq.SafeChecker.PCUICSafeConversion]
Conversion.X [in MetaRocq.SafeChecker.PCUICSafeConversion]
Conversion.X_type [in MetaRocq.SafeChecker.PCUICSafeConversion]
Conversion.Σ [in MetaRocq.Template.Checker]
ConvRedConv.cf [in MetaRocq.PCUIC.PCUICConversion]
ConvRedConv.wfΣ [in MetaRocq.PCUIC.PCUICConversion]
ConvRedConv.Σ [in MetaRocq.PCUIC.PCUICConversion]
ConvSubst.cf [in MetaRocq.PCUIC.PCUICConversion]
ConvSubst.wfΣ [in MetaRocq.PCUIC.PCUICConversion]
ConvSubst.Σ [in MetaRocq.PCUIC.PCUICConversion]
ConvTerms.cf [in MetaRocq.PCUIC.PCUICConversion]
ConvTerms.wfΣ [in MetaRocq.PCUIC.PCUICConversion]
ConvTerms.Σ [in MetaRocq.PCUIC.PCUICConversion]
CtxInstSize.cf [in MetaRocq.PCUIC.PCUICTyping]
CtxInstSize.typing [in MetaRocq.PCUIC.PCUICTyping]
CtxInstSize.typing [in MetaRocq.Template.Typing]
CtxInstSize.typing_size [in MetaRocq.PCUIC.PCUICTyping]
CtxInstSize.typing_size [in MetaRocq.Template.Typing]
CtxReduction.cf [in MetaRocq.PCUIC.PCUICSubstitution]
CtxReduction.cf [in MetaRocq.PCUIC.PCUICContextReduction]
CtxReduction.wfΣ [in MetaRocq.PCUIC.PCUICSubstitution]
CtxReduction.wfΣ [in MetaRocq.PCUIC.PCUICContextReduction]
CtxReduction.Σ [in MetaRocq.PCUIC.PCUICSubstitution]
CtxReduction.Σ [in MetaRocq.PCUIC.PCUICContextReduction]
CumulSpecIsCumulAlgo.cf [in MetaRocq.PCUIC.PCUICConversion]
CumulSpecIsCumulAlgo.cf [in MetaRocq.PCUIC.PCUICConversion]
CumulSpecIsCumulAlgo.wfΣ [in MetaRocq.PCUIC.PCUICConversion]
CumulSpecIsCumulAlgo.Σ [in MetaRocq.PCUIC.PCUICConversion]
CumulSpecIsCumulAlgo.Σ [in MetaRocq.PCUIC.PCUICConversion]
CumulSubst.cf [in MetaRocq.PCUIC.PCUICConversion]
CumulSubst.wfΣ [in MetaRocq.PCUIC.PCUICConversion]
CumulSubst.Σ [in MetaRocq.PCUIC.PCUICConversion]

---

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