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)

H

HasLen [record, in MetaRocq.PCUIC.PCUICAst]
HasLen [inductive, in MetaRocq.PCUIC.PCUICAst]
has_sort_isType [definition, in MetaRocq.PCUIC.PCUICTyping]
has_nparams [definition, in MetaRocq.PCUIC.PCUICTyping]
has_atom [definition, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
has_bit [definition, in MetaRocq.Erasure.Typed.Optimize]
has_atom [definition, in MetaRocq.Erasure.EWcbvEvalEtaInd]
has_atom [definition, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
has_nparams [definition, in MetaRocq.Template.Typing]
has_prim_map_prim [lemma, in MetaRocq.Erasure.EWellformed]
has_prim_all_primitive_flags [lemma, in MetaRocq.Erasure.EWellformed]
has_cstr_params [projection, in MetaRocq.Erasure.EWellformed]
has_axioms [projection, in MetaRocq.Erasure.EWellformed]
has_tLazy_Force [projection, in MetaRocq.Erasure.EWellformed]
has_tPrim [projection, in MetaRocq.Erasure.EWellformed]
has_tCoFix [projection, in MetaRocq.Erasure.EWellformed]
has_tFix [projection, in MetaRocq.Erasure.EWellformed]
has_tProj [projection, in MetaRocq.Erasure.EWellformed]
has_tCase [projection, in MetaRocq.Erasure.EWellformed]
has_tConstruct [projection, in MetaRocq.Erasure.EWellformed]
has_tConst [projection, in MetaRocq.Erasure.EWellformed]
has_tApp [projection, in MetaRocq.Erasure.EWellformed]
has_tLetIn [projection, in MetaRocq.Erasure.EWellformed]
has_tLambda [projection, in MetaRocq.Erasure.EWellformed]
has_tEvar [projection, in MetaRocq.Erasure.EWellformed]
has_tVar [projection, in MetaRocq.Erasure.EWellformed]
has_tRel [projection, in MetaRocq.Erasure.EWellformed]
has_tBox [projection, in MetaRocq.Erasure.EWellformed]
has_prim [definition, in MetaRocq.Erasure.EWellformed]
has_primarray [projection, in MetaRocq.Erasure.EWellformed]
has_primstring [projection, in MetaRocq.Erasure.EWellformed]
has_primfloat [projection, in MetaRocq.Erasure.EWellformed]
has_primint [projection, in MetaRocq.Erasure.EWellformed]
hd_error_skipn_iff_In [lemma, in MetaRocq.Utils.MRList]
head [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
head [definition, in MetaRocq.Quotation.ToPCUIC.Init]
head [definition, in MetaRocq.Quotation.ToTemplate.Init]
head [definition, in MetaRocq.Erasure.EAstUtils]
Head [library]
HeadMismatch [constructor, in MetaRocq.SafeChecker.PCUICErrors]
head_tapp [lemma, in MetaRocq.Erasure.EImplementBox]
head_mkApps [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
head_tapp [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
head_nApp [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
head_arguments [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
head_term_is_bound [definition, in MetaRocq.Quotation.ToPCUIC.Init]
head_nApp [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
head_term_is_bound [definition, in MetaRocq.Quotation.ToTemplate.Init]
head_tapp [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
head_subst [lemma, in MetaRocq.PCUIC.PCUICInductives]
head_mkApps [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
head_mkApps_nApp [lemma, in MetaRocq.Erasure.EAstUtils]
head_nApp_eq [lemma, in MetaRocq.Erasure.EAstUtils]
head_nApp [lemma, in MetaRocq.Erasure.EAstUtils]
head_tApp [lemma, in MetaRocq.Erasure.EAstUtils]
head_mkApps [lemma, in MetaRocq.Erasure.EAstUtils]
heΣ [definition, in MetaRocq.Erasure.Typed.Erasure]
heΣ [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
heΣ [definition, in MetaRocq.Erasure.ErasureFunction]
heΣ [definition, in MetaRocq.SafeChecker.PCUICSafeRetyping]
heΣ [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
heΣ [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
heΣ [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
hint_locality [inductive, in MetaRocq.Template.TemplateMonad.Common]
Hlookup [definition, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
Hlookup_env [definition, in MetaRocq.Erasure.ErasureFunction]
hnf [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
hnf [constructor, in MetaRocq.Template.TemplateMonad.Common]
hnf [abbreviation, in MetaRocq.SafeChecker.PCUICTypeChecker]
hnf_complete [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
hnf_sound [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
hnf_stack [definition, in MetaRocq.Template.Checker]
hnf_subterm_rel [definition, in MetaRocq.SafeChecker.PCUICWfReduction]
hole [definition, in MetaRocq.Template.Ast]
hole_branch_context [definition, in MetaRocq.PCUIC.PCUICReduction]
hole_list_context [definition, in MetaRocq.PCUIC.PCUICReduction]
hole_context [definition, in MetaRocq.PCUIC.PCUICReduction]
hyp [projection, in MetaRocq.Erasure.EInduction]
Hyp [record, in MetaRocq.Erasure.EInduction]
hyp [constructor, in MetaRocq.Erasure.EInduction]
Hyp [inductive, in MetaRocq.Erasure.EInduction]
HypH [constructor, in MetaRocq.Utils.LibHypsNaming]
HypH_ [constructor, in MetaRocq.Utils.LibHypsNaming]
HypNone [constructor, in MetaRocq.Utils.LibHypsNaming]
HypPrefixes [inductive, in MetaRocq.Utils.LibHypsNaming]
HypPrefixes_sind [definition, in MetaRocq.Utils.LibHypsNaming]
HypPrefixes_rec [definition, in MetaRocq.Utils.LibHypsNaming]
HypPrefixes_ind [definition, in MetaRocq.Utils.LibHypsNaming]
HypPrefixes_rect [definition, in MetaRocq.Utils.LibHypsNaming]
hyps [projection, in MetaRocq.Examples.tauto]
hyps_size_app [lemma, in MetaRocq.Examples.tauto]
hyps_size [definition, in MetaRocq.Examples.tauto]
HΣ [definition, in MetaRocq.Erasure.Typed.Erasure]
hΣ [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
HΣ [definition, in MetaRocq.Erasure.ErasureFunction]
hΣ [definition, in MetaRocq.SafeChecker.PCUICSafeRetyping]
hΣ [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
hΣ [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
hΣ [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
HΣ' [definition, in MetaRocq.SafeChecker.PCUICWfEnvImpl]

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)