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)

---

T (variable)

TransformExt.Comp.env [in MetaRocq.Erasure.EProgram]
TransformExt.Comp.env' [in MetaRocq.Erasure.EProgram]
TransformExt.Comp.env'' [in MetaRocq.Erasure.EProgram]
TransformExt.Comp.eval [in MetaRocq.Erasure.EProgram]
TransformExt.Comp.eval' [in MetaRocq.Erasure.EProgram]
TransformExt.Comp.eval'' [in MetaRocq.Erasure.EProgram]
TransformExt.Comp.extends [in MetaRocq.Erasure.EProgram]
TransformExt.Comp.extends' [in MetaRocq.Erasure.EProgram]
TransformExt.Comp.extends'' [in MetaRocq.Erasure.EProgram]
TransformExt.Comp.term [in MetaRocq.Erasure.EProgram]
TransformExt.Comp.term' [in MetaRocq.Erasure.EProgram]
TransformExt.Comp.term'' [in MetaRocq.Erasure.EProgram]
TransformExt.Comp.value [in MetaRocq.Erasure.EProgram]
TransformExt.Comp.value' [in MetaRocq.Erasure.EProgram]
TransformExt.Comp.value'' [in MetaRocq.Erasure.EProgram]
TransformExt.Opt.env [in MetaRocq.Erasure.EProgram]
TransformExt.Opt.env' [in MetaRocq.Erasure.EProgram]
TransformExt.Opt.env'' [in MetaRocq.Erasure.EProgram]
TransformExt.Opt.eval [in MetaRocq.Erasure.EProgram]
TransformExt.Opt.eval' [in MetaRocq.Erasure.EProgram]
TransformExt.Opt.eval'' [in MetaRocq.Erasure.EProgram]
TransformExt.Opt.extends [in MetaRocq.Erasure.EProgram]
TransformExt.Opt.extends' [in MetaRocq.Erasure.EProgram]
TransformExt.Opt.o [in MetaRocq.Erasure.EProgram]
TransformExt.Opt.term [in MetaRocq.Erasure.EProgram]
TransformExt.Opt.term' [in MetaRocq.Erasure.EProgram]
TransformExt.Opt.term'' [in MetaRocq.Erasure.EProgram]
TransformExt.Opt.value [in MetaRocq.Erasure.EProgram]
TransformExt.Opt.value' [in MetaRocq.Erasure.EProgram]
TransformExt.Opt.value'' [in MetaRocq.Erasure.EProgram]
transform_blocks.Σ [in MetaRocq.Erasure.EConstructorsAsBlocks]
Transform.Comp.env [in MetaRocq.Common.Transform]
Transform.Comp.env' [in MetaRocq.Common.Transform]
Transform.Comp.env'' [in MetaRocq.Common.Transform]
Transform.Comp.eval [in MetaRocq.Common.Transform]
Transform.Comp.eval' [in MetaRocq.Common.Transform]
Transform.Comp.eval'' [in MetaRocq.Common.Transform]
Transform.Comp.term [in MetaRocq.Common.Transform]
Transform.Comp.term' [in MetaRocq.Common.Transform]
Transform.Comp.term'' [in MetaRocq.Common.Transform]
Transform.Comp.value [in MetaRocq.Common.Transform]
Transform.Comp.value' [in MetaRocq.Common.Transform]
Transform.Comp.value'' [in MetaRocq.Common.Transform]
Transform.Opt.env [in MetaRocq.Common.Transform]
Transform.Opt.env' [in MetaRocq.Common.Transform]
Transform.Opt.eval [in MetaRocq.Common.Transform]
Transform.Opt.eval' [in MetaRocq.Common.Transform]
Transform.Opt.term [in MetaRocq.Common.Transform]
Transform.Opt.term' [in MetaRocq.Common.Transform]
Transform.Opt.value [in MetaRocq.Common.Transform]
Transform.Opt.value' [in MetaRocq.Common.Transform]
Translation.Σ [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_lookups.g [in MetaRocq.Erasure.ErasureProperties]
trans_lookups.Σ' [in MetaRocq.Erasure.ErasureProperties]
trans_lookups.Σ [in MetaRocq.Erasure.ErasureProperties]
Trans_Global.wfΣ' [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Trans_Global.wfΣ [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Trans_Global.Σ [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Trans_Global.cf [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Trans_Global.wfΣ' [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Trans_Global.wfΣ [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Trans_Global.Σ [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Trans_Global.cf [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Trans_Global.wfΣ' [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Trans_Global.wfΣ [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Trans_Global.Σ [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Trans_Global.cf [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Trans.Σ [in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans.Σ [in MetaRocq.Erasure.ECoInductiveToInductive]
TraverseWithBindersM.a [in MetaRocq.Template.AstUtils]
TraverseWithBindersM.A [in MetaRocq.Template.AstUtils]
TraverseWithBindersM.Acc [in MetaRocq.Template.AstUtils]
TraverseWithBindersM.liftM [in MetaRocq.Template.AstUtils]
TraverseWithBindersM.M [in MetaRocq.Template.AstUtils]
TraverseWithBinders.a [in MetaRocq.Template.AstUtils]
TraverseWithBinders.A [in MetaRocq.Template.AstUtils]
TraverseWithBinders.Acc [in MetaRocq.Template.AstUtils]
TraverseWithBinders.lift [in MetaRocq.Template.AstUtils]
Typecheck.cf [in MetaRocq.Template.Checker]
Typecheck.cf [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_primitive.wfΓ [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_primitive.Γ [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_primitive.infer [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_mfix.wfΓ [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_mfix.Γ [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_mfix.infer [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.hpctx [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.ptm [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.wfpret [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.predctx [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.wfp [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.hty [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.isdecl [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.args [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.p [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.idecl [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.mdecl [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.ci [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.ps [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.wfΓ [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.Γ [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.infer [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.F [in MetaRocq.Template.Checker]
Typecheck.F [in MetaRocq.Template.Checker]
Typecheck.G [in MetaRocq.Template.Checker]
Typecheck.InferAux.infer [in MetaRocq.Template.Checker]
Typecheck.InferAux.infer [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.make_All.f [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.make_All.B [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.make_All.A [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.nor [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.normalization_in [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.X [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.X_type [in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.Σ [in MetaRocq.Template.Checker]
Typecheck.Σ [in MetaRocq.Template.Checker]
TypeOf.cf [in MetaRocq.SafeChecker.PCUICSafeRetyping]
TypeOf.nor [in MetaRocq.SafeChecker.PCUICSafeRetyping]
TypeOf.normalization_in [in MetaRocq.SafeChecker.PCUICSafeRetyping]
TypeOf.X [in MetaRocq.SafeChecker.PCUICSafeRetyping]
TypeOf.X_type [in MetaRocq.SafeChecker.PCUICSafeRetyping]
TypingWf.cf [in MetaRocq.Template.TypingWf]
Typing_Spine_size.Γ [in MetaRocq.Template.Typing]
Typing_Spine_size.Σ [in MetaRocq.Template.Typing]
Typing_Spine_size.fn [in MetaRocq.Template.Typing]
Typing_Spine_size.Γ [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
Typing_Spine_size.Σ [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]

---

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