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)

---

P (variable)

ParallelReduction.Σ [in MetaRocq.PCUIC.PCUICParallelReduction]
ParallelSubstitution.cf [in MetaRocq.PCUIC.PCUICParallelReduction]
ParallelSubstitution.Σ [in MetaRocq.PCUIC.PCUICParallelReduction]
ParallelWeakening.cf [in MetaRocq.PCUIC.PCUICParallelReduction]
pipeline_theorem.v_t [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.Σ_v [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.t_t [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.Σ_t [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.Heval [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.fo [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.typing [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.Normalisation [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.args [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.u [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.i [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.v [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.axfree [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.expt [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.t [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.expΣ [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.HΣ [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.Σ [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_cond.v_t [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_cond.Σ_v [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_cond.t_t [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_cond.Σ_t [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_cond.Heval [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_cond.v [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_cond.Normalisation [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_cond.typing [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_cond.expt [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_cond.expΣ [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_cond.HΣ [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_cond.T [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_cond.t [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_cond.Σ [in MetaRocq.ErasurePlugin.ErasureCorrectness]
PredRed.cf [in MetaRocq.PCUIC.PCUICConfluence]
PredRed.wfΣ [in MetaRocq.PCUIC.PCUICConfluence]
PredRed.Σ [in MetaRocq.PCUIC.PCUICConfluence]
PrimDeps.deps [in MetaRocq.Erasure.EAstUtils]
PrimIn.term [in MetaRocq.Erasure.EPrimitive]
PrimitiveSize.cf [in MetaRocq.PCUIC.PCUICTyping]
PrimitiveSize.typing [in MetaRocq.PCUIC.PCUICTyping]
PrimitiveSize.typing_size [in MetaRocq.PCUIC.PCUICTyping]
PrimModel.term [in MetaRocq.Erasure.EPrimitive]
PrimOps.term [in MetaRocq.Erasure.EPrimitive]
PrimOps.term' [in MetaRocq.Erasure.EPrimitive]
primtheory.f [in MetaRocq.Erasure.EPrimitive]
primtheory.g [in MetaRocq.Erasure.EPrimitive]
primtheory.p [in MetaRocq.Erasure.EPrimitive]
primtheory.p [in MetaRocq.Erasure.EPrimitive]
primtheory.term [in MetaRocq.Erasure.EPrimitive]
primtheory.term [in MetaRocq.Erasure.EPrimitive]
primtheory.term' [in MetaRocq.Erasure.EPrimitive]
primtheory.term'' [in MetaRocq.Erasure.EPrimitive]
Principality.cf [in MetaRocq.PCUIC.PCUICPrincipality]
Principality.wfΣ [in MetaRocq.PCUIC.PCUICPrincipality]
Principality.Σ [in MetaRocq.PCUIC.PCUICPrincipality]
PrintTermTree.env.all [in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.env.Aux.print_term [in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.env.with_universes [in MetaRocq.Template.Pretty]
PrintTermTree.env.Σ [in MetaRocq.Template.Pretty]
PrintTermTree.env.Σ [in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.env.Σ [in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_term.Σ [in MetaRocq.Erasure.EPretty]
print_term.Σ [in MetaRocq.Template.Pretty]
PTree.COMBINE.A [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.COMBINE.B [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.COMBINE.C [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.COMBINE.f [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.COMBINE.f_None_None [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.MAP_FILTER.B [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.MAP_FILTER.A [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_IND.node [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_IND.empty [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_IND.P [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_IND.A [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_REC.node_empty [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_REC.node [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_REC.empty [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_REC.B [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_REC.A [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_CASE.node_empty [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_CASE.node [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_CASE.empty [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_CASE.B [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_CASE.A [in MetaRocq.Utils.canonicaltries.CanonicalTries]

---

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