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)

---

R (constructor)

Reduction [in MetaRocq.SafeChecker.PCUICSafeConversion]
red_view_other [in MetaRocq.SafeChecker.PCUICSafeReduce]
red_view_Proj [in MetaRocq.SafeChecker.PCUICSafeReduce]
red_view_Case [in MetaRocq.SafeChecker.PCUICSafeReduce]
red_view_Fix [in MetaRocq.SafeChecker.PCUICSafeReduce]
red_view_Lambda [in MetaRocq.SafeChecker.PCUICSafeReduce]
red_view_App [in MetaRocq.SafeChecker.PCUICSafeReduce]
red_view_Const [in MetaRocq.SafeChecker.PCUICSafeReduce]
red_view_LetIn [in MetaRocq.SafeChecker.PCUICSafeReduce]
red_view_Rel [in MetaRocq.SafeChecker.PCUICSafeReduce]
red_proj [in MetaRocq.Template.Typing]
red_delta [in MetaRocq.Template.Typing]
red_cofix_proj [in MetaRocq.Template.Typing]
red_cofix_case [in MetaRocq.Template.Typing]
red_fix [in MetaRocq.Template.Typing]
red_iota [in MetaRocq.Template.Typing]
red_rel [in MetaRocq.Template.Typing]
red_zeta [in MetaRocq.Template.Typing]
red_beta [in MetaRocq.Template.Typing]
red_vdef_body [in MetaRocq.PCUIC.PCUICReduction]
red_vass [in MetaRocq.PCUIC.PCUICReduction]
red_proj [in MetaRocq.PCUIC.PCUICReduction]
red_delta [in MetaRocq.PCUIC.PCUICReduction]
red_cofix_proj [in MetaRocq.PCUIC.PCUICReduction]
red_cofix_case [in MetaRocq.PCUIC.PCUICReduction]
red_fix [in MetaRocq.PCUIC.PCUICReduction]
red_iota [in MetaRocq.PCUIC.PCUICReduction]
red_rel [in MetaRocq.PCUIC.PCUICReduction]
red_zeta [in MetaRocq.PCUIC.PCUICReduction]
red_beta [in MetaRocq.PCUIC.PCUICReduction]
Red1Apps.abs_red_r [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.abs_red_l [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.app_fix_red_body [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.app_fix_red_ty [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.app_red_r [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.app_red_l [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.array_red_type [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.array_red_def [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.array_red_val [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.case_red_brs [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.case_red_discr [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.case_red_return [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.case_red_param [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.cofix_red_body [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.cofix_red_ty [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.evar_red [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.fix_red_body [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.fix_red_ty [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.letin_red_body [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.letin_red_ty [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.letin_red_def [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.prod_red_r [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.prod_red_l [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.proj_red [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red_proj [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red_delta [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red_cofix_proj [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red_cofix_case [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red_fix [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red_iota [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red_rel [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red_zeta [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red_beta [in MetaRocq.PCUIC.PCUICEtaExpand]
ReflectF [in MetaRocq.Utils.MRReflect]
reflectF [in MetaRocq.Utils.ReflectEq]
reflectP [in MetaRocq.Utils.ReflectEq]
ReflectT [in MetaRocq.Utils.MRReflect]
refl_red [in MetaRocq.Template.Typing]
refl_redl [in MetaRocq.PCUIC.PCUICReduction]
Relevant [in MetaRocq.Common.BasicAst]
RelInductive [in MetaRocq.Erasure.Typed.Erasure]
RelOther [in MetaRocq.Erasure.Typed.Erasure]
RelTypeVar [in MetaRocq.Erasure.Typed.Erasure]
rel_none [in MetaRocq.PCUIC.PCUICEquality]
rel_some [in MetaRocq.PCUIC.PCUICEquality]
represents_value_tLazy [in MetaRocq.Erasure.EWcbvEvalNamed]
represents_value_tPrim [in MetaRocq.Erasure.EWcbvEvalNamed]
represents_value_tFix [in MetaRocq.Erasure.EWcbvEvalNamed]
represents_value_tConstruct [in MetaRocq.Erasure.EWcbvEvalNamed]
represents_value_tClos [in MetaRocq.Erasure.EWcbvEvalNamed]
represents_tForce [in MetaRocq.Erasure.EWcbvEvalNamed]
represents_tLazy [in MetaRocq.Erasure.EWcbvEvalNamed]
represents_tPrim [in MetaRocq.Erasure.EWcbvEvalNamed]
represents_tFix [in MetaRocq.Erasure.EWcbvEvalNamed]
represents_tCase [in MetaRocq.Erasure.EWcbvEvalNamed]
represents_tConstruct [in MetaRocq.Erasure.EWcbvEvalNamed]
represents_tConst [in MetaRocq.Erasure.EWcbvEvalNamed]
represents_tApp [in MetaRocq.Erasure.EWcbvEvalNamed]
represents_tLetIn [in MetaRocq.Erasure.EWcbvEvalNamed]
represents_tLambda [in MetaRocq.Erasure.EWcbvEvalNamed]
represents_unbound_tRel [in MetaRocq.Erasure.EWcbvEvalNamed]
represents_bound_tRel [in MetaRocq.Erasure.EWcbvEvalNamed]
rho_fix_stuck [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_fix_red [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
right_dlexmod [in MetaRocq.PCUIC.utils.PCUICUtils]
right_lex [in MetaRocq.PCUIC.utils.PCUICUtils]
rt_ctx_t_trans [in MetaRocq.PCUIC.PCUICConfluence]
rt_ctx_t_refl [in MetaRocq.PCUIC.PCUICConfluence]
rt_ctx_t_step [in MetaRocq.PCUIC.PCUICConfluence]
rt_ctx_trans [in MetaRocq.PCUIC.PCUICConfluence]
rt_ctx_refl [in MetaRocq.PCUIC.PCUICConfluence]
rt_ctx_step [in MetaRocq.PCUIC.PCUICConfluence]
rt_ctx_decl_trans [in MetaRocq.PCUIC.PCUICConfluence]
rt_ctx_decl_refl [in MetaRocq.PCUIC.PCUICConfluence]
rt_ctx_decl_step [in MetaRocq.PCUIC.PCUICConfluence]
rt1n_ctx_trans [in MetaRocq.PCUIC.PCUICConfluence]
rt1n_ctx_eq [in MetaRocq.PCUIC.PCUICConfluence]

---

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)

Generated by coqdoc and improved with CoqdocJS