Global Index

(75519 entries)

Notation Index

A

B

D

F

H

J

L

O

Q

R

U

X

Y

Z

_

(245 entries)

Binder Index

(61331 entries)

Module Index

H

J

Q

X

Y

Z

_

other

(144 entries)

Variable Index

D

G

H

J

K

L

P

Q

U

V

X

Y

Z

_

other

(89 entries)

Library Index

F

G

H

J

O

Q

V

X

Y

Z

_

other

(236 entries)

Lemma Index

J

Y

_

other

(6913 entries)

Constructor Index

J

K

X

Y

Z

_

other

(1141 entries)

Axiom Index

B

D

E

H

I

J

K

L

M

O

P

Q

R

S

V

W

X

Y

Z

_

other

(34 entries)

Inductive Index

J

K

X

Y

Z

_

other

(269 entries)

Projection Index

J

X

Y

Z

_

(443 entries)

Section Index

H

J

K

Q

X

Y

Z

_

other

(296 entries)

Instance Index

H

X

Y

_

other

(604 entries)

Abbreviation Index

J

K

Q

X

Z

_

(248 entries)

Definition Index

Y

(3386 entries)

Record Index

J

K

L

X

Y

Z

_

other

(140 entries)

S (projection)

snd' [in MetaCoq.Examples.demo]
spine_codom_wf [in MetaCoq.PCUIC.PCUICSpine]
spine_dom_wf [in MetaCoq.PCUIC.PCUICSpine]
st [in MetaCoq.SafeChecker.PCUICSafeConversion]
stk1 [in MetaCoq.SafeChecker.PCUICSafeConversion]
stk2 [in MetaCoq.SafeChecker.PCUICSafeConversion]
subst_instance [in MetaCoq.Template.Universes]
symmetry [in MetaCoq.Translations.MiniHoTT]
symmetry [in MetaCoq.Translations.MiniHoTT_paths]