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

(18986 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

(297 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

(8135 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

(1490 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

(343 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

(524 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

(720 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

(401 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

(331 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

(4701 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

(178 entries)

C (inductive)

case_branch_typing [in MetaRocq.PCUIC.PCUICTyping]
case_side_conditions [in MetaRocq.PCUIC.PCUICTyping]
case_inversion_data [in MetaRocq.PCUIC.PCUICInversion]
cast_kind [in MetaRocq.Common.BasicAst]
checking [in MetaRocq.PCUIC.Bidirectional.BDTyping]
choice [in MetaRocq.PCUIC.Syntax.PCUICPosition]
clos_refl_trans_ctx_1n [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_t [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_decl [in MetaRocq.PCUIC.PCUICConfluence]
cls_is_true [in MetaRocq.Quotation.CommonUtils]
constant_entry [in MetaRocq.PCUIC.PCUICAst]
constant_entry [in MetaRocq.Erasure.EAst]
constant_entry [in MetaRocq.Template.Ast]
ConstraintType.lt_ [in MetaRocq.Common.Universes]
ConstraintType.t_ [in MetaRocq.Common.Universes]
construct_cofix_view [in MetaRocq.SafeChecker.PCUICSafeReduce]
construct_view [in MetaRocq.SafeChecker.PCUICSafeReduce]
construct_view [in MetaRocq.Erasure.EEtaExpanded]
construct_cofix_view [in MetaRocq.PCUIC.Syntax.PCUICViews]
construct0_cofix_view [in MetaRocq.SafeChecker.PCUICSafeReduce]
construct0_cofix_view [in MetaRocq.PCUIC.Syntax.PCUICViews]
contextual_closure [in MetaRocq.PCUIC.PCUICReduction]
context_subst [in MetaRocq.PCUIC.PCUICContextSubst]
context_decl_hole [in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_decl_choice [in MetaRocq.PCUIC.Syntax.PCUICPosition]
ConversionError [in MetaRocq.SafeChecker.PCUICErrors]
ConversionResult [in MetaRocq.SafeChecker.PCUICSafeConversion]
ConversionResultSummary [in MetaRocq.SafeChecker.PCUICSafeConversion]
Conversion.All_decls_alpha_pb [in MetaRocq.Common.EnvironmentTyping]
conv_pb [in MetaRocq.Common.BasicAst]
conv_pb [in MetaRocq.Template.Checker]
cored [in MetaRocq.PCUIC.PCUICSafeLemmata]
cumulAlgo_gen [in MetaRocq.PCUIC.PCUICCumulativity]
cumulP [in MetaRocq.PCUIC.PCUICSubstitution]
cumulSpec0 [in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_gen [in MetaRocq.Template.Typing]
cumul_prop [in MetaRocq.PCUIC.PCUICCumulProp]

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

(18986 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

(297 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

(8135 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

(1490 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

(343 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

(524 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

(720 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

(401 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

(331 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

(4701 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

(178 entries)