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)

---

I (abbreviation)

inst_branches [in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_branch [in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_predicate [in MetaRocq.PCUIC.PCUICSigmaCalculus]
invert_red_ind [in MetaRocq.PCUIC.PCUICConversion]
isconv_fallback [in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_args [in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_prog [in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_red [in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_fallback_raw [in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_args_raw [in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_prog_raw [in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_red_raw [in MetaRocq.SafeChecker.PCUICSafeConversion]
isEtaExp [in MetaRocq.Erasure.EEtaExpanded]
isEtaExp [in MetaRocq.Erasure.EEtaExpanded]
isWAT [in MetaRocq.PCUIC.PCUICArities]
is_open_mfix [in MetaRocq.PCUIC.PCUICConversion]
is_open_def [in MetaRocq.PCUIC.PCUICConversion]
is_open_predicate [in MetaRocq.PCUIC.PCUICConversion]
is_open_brs [in MetaRocq.PCUIC.PCUICConversion]
is_expanded_env [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_expanded [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_expanded_aux [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_closed_context [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
is_open_decl [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
is_open_term [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]

Generated by coqdoc and improved with CoqdocJS