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

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

(245 entries)

Binder 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

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

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

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

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

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

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

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

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

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

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

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

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

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

(140 entries)

O (definition)

occ_betweenP [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
odd [in MetaCoq.Examples.demo]
oi [in MetaCoq.PCUIC.PCUICInductives]
oib [in MetaCoq.PCUIC.PCUICInductives]
onctx_k [in MetaCoq.Template.BasicAst]
onctx_rel [in MetaCoq.PCUIC.Syntax.PCUICInduction]
onctx_rel [in MetaCoq.PCUIC.Syntax.PCUICDepth]
ondecl [in MetaCoq.Template.BasicAst]
ones [in MetaCoq.Examples.demo]
one_pt_i [in MetaCoq.Examples.demo]
one_list_i [in MetaCoq.Examples.demo]
one_i2 [in MetaCoq.Examples.demo]
one_i [in MetaCoq.Examples.demo]
on_global_univ_init_env [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
on_udecl_prop [in MetaCoq.PCUIC.PCUICWeakeningEnv]
on_Trel [in MetaCoq.Template.utils.MCRelations]
on_rel [in MetaCoq.Template.utils.MCRelations]
on_fst [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
on_ctx_universes [in MetaCoq.PCUIC.PCUICWfUniverses]
on_decl_universes [in MetaCoq.PCUIC.PCUICWfUniverses]
on_universes [in MetaCoq.PCUIC.PCUICWfUniverses]
on_pair [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
on_wf_local_decl [in MetaCoq.Template.Typing]
on_one_decl [in MetaCoq.PCUIC.utils.PCUICOnOne]
on_free_vars_ctx_k [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_terms [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_decl [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_inl [in MetaCoq.Template.common.uGraph]
on_subterm [in MetaCoq.SafeChecker.PCUICSafeRetyping]
on_free_vars_mfix [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
on_fst [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_ctxs [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
on_free_vars_decls [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
on_hyps [in MetaCoq.Examples.tauto]
on_hyp [in MetaCoq.Examples.tauto]
on_Some_or_None [in MetaCoq.Template.utils.MCOption]
on_Some [in MetaCoq.Template.utils.MCOption]
on_some [in MetaCoq.Template.utils.MCOption]
on_wf_local_decl [in MetaCoq.PCUIC.PCUICTyping]
on_local_decl_glob [in MetaCoq.PCUIC.PCUICTyping]
on_pi2 [in MetaCoq.Template.utils.MCProd]
on_snd [in MetaCoq.Template.utils.MCProd]
on_local_decl [in MetaCoq.PCUIC.PCUICContextConversion]
on_local_decl [in MetaCoq.PCUIC.Syntax.PCUICInduction]
on_ctx_free_vars_fold [in MetaCoq.PCUIC.PCUICContextReduction]
on_option [in MetaCoq.Template.TypingWf]
open_decl_proj [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
open_decl [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
optimize [in MetaCoq.Erasure.EInlineProjections]
optimize [in MetaCoq.Erasure.EOptimizePropDiscr]
optimized_abstract_env_impl [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
optimized_abstract_env_ext_impl [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
optimize_program_expanded [in MetaCoq.Erasure.EInlineProjections]
optimize_program_wf [in MetaCoq.Erasure.EInlineProjections]
optimize_program [in MetaCoq.Erasure.EInlineProjections]
optimize_env' [in MetaCoq.Erasure.EInlineProjections]
optimize_env [in MetaCoq.Erasure.EInlineProjections]
optimize_decl [in MetaCoq.Erasure.EInlineProjections]
optimize_constant_decl [in MetaCoq.Erasure.EInlineProjections]
optimize_prop_discr_optimization [in MetaCoq.Erasure.ETransform]
optimize_program_expanded [in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_program_wf [in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_program [in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_env' [in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_env [in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_decl [in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_constant_decl [in MetaCoq.Erasure.EOptimizePropDiscr]
optim_make_wf_env_ext [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
optim_pop [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
option_is_none [in MetaCoq.Erasure.Extract]
option_edge_of_level [in MetaCoq.Template.common.uGraph]
option_default [in MetaCoq.Template.utils.MCOption]
option_get [in MetaCoq.Template.utils.MCOption]
opt_bool_to_bool [in MetaCoq.Template.Checker]
opt_wcbv_flags [in MetaCoq.Erasure.EWcbvEval]
OT_byte.eq_dec [in MetaCoq.Template.utils.bytestring]
OT_byte.compare [in MetaCoq.Template.utils.bytestring]
OT_byte.lt [in MetaCoq.Template.utils.bytestring]
OT_byte.eq [in MetaCoq.Template.utils.bytestring]
OT_byte.t [in MetaCoq.Template.utils.bytestring]

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

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

(245 entries)

Binder 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

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

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

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

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

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

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

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

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

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

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

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

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

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

(140 entries)