Global Index

A

B

D

E

F

G

H

J

K

M

O

P

Q

R

S

U

V

W

X

Y

Z

_

(180 entries)

Axiom Index

A

B

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

U

V

W

X

Y

Z

_

(3 entries)

Lemma Index

A

B

C

D

E

F

G

H

I

J

K

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(63 entries)

Constructor Index

A

B

D

E

F

G

H

I

J

K

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(39 entries)

Inductive Index

A

B

D

E

F

G

H

I

J

K

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(14 entries)

Definition Index

A

B

D

E

F

G

H

J

K

M

O

P

Q

R

S

U

V

W

X

Y

Z

_

(57 entries)

Module Index

A

B

D

E

F

G

H

I

J

K

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(3 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

L

M

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(1 entry)

Global Index

C

C [module, in nbe]
constants [axiom, in nbe]
Constants [module, in nbe]
constant_types [axiom, in nbe]
csts [inductive, in nbe]
cst_bool [constructor, in nbe]
cst_bool_t [constructor, in nbe]
cst_nat [constructor, in nbe]
cst_nat_t [constructor, in nbe]
cst_types [inductive, in nbe]
C.constants [definition, in nbe]
C.constant_types [definition, in nbe]
C.type_constant [definition, in nbe]

I

interp_closed_nb [definition, in nbe]
interp_constant [definition, in nbe]
interp_constant_type [definition, in nbe]
interp_nb [definition, in nbe]
interp_nb_type [definition, in nbe]

L

L [module, in nbe]
L.app [constructor, in nbe]
L.append [definition, in nbe]
L.app_assoc [lemma, in nbe]
L.app_empty [lemma, in nbe]
L.augment_valuation [definition, in nbe]
L.coerce_neutral_context [definition, in nbe]
L.coerce_nf_context [definition, in nbe]
L.coerce_subst_context [definition, in nbe]
L.coerce_term_context [definition, in nbe]
L.coerce_term_context_id [lemma, in nbe]
L.coerce_term_context_lift_rec [lemma, in nbe]
L.coerce_term_context_lift_rec_aux [lemma, in nbe]
L.coerce_var_context [definition, in nbe]
L.coerce_var_context_id [lemma, in nbe]
L.coerce_var_context_lift_var [lemma, in nbe]
L.comma [constructor, in nbe]
L.conv [inductive, in nbe]
L.conv_app [constructor, in nbe]
L.conv_lam [constructor, in nbe]
L.conv_red [constructor, in nbe]
L.conv_refl [constructor, in nbe]
L.conv_sym [constructor, in nbe]
L.conv_trans [constructor, in nbe]
L.cst [constructor, in nbe]
L.ctx [inductive, in nbe]
L.empty [constructor, in nbe]
L.eq_rect_coerce [lemma, in nbe]
L.eq_rect_coerce_var [lemma, in nbe]
L.evaluates [inductive, in nbe]
L.eval_cst [constructor, in nbe]
L.eval_lam [constructor, in nbe]
L.eval_trans [constructor, in nbe]
L.first [constructor, in nbe]
L.interp_closed_term [definition, in nbe]
L.interp_term [definition, in nbe]
L.interp_type [definition, in nbe]
L.is_normalizing [definition, in nbe]
L.is_normalizing_app [definition, in nbe]
L.lam [constructor, in nbe]
L.lift [definition, in nbe]
L.lift_ctx [definition, in nbe]
L.lift_lift [lemma, in nbe]
L.lift_lift_stmt [definition, in nbe]
L.lift_lift_var [lemma, in nbe]
L.lift_lift_var_stmt [definition, in nbe]
L.lift_rec [definition, in nbe]
L.lift_rec_comma_first [lemma, in nbe]
L.lift_rec_comma_next [lemma, in nbe]
L.lift_rec_empty [lemma, in nbe]
L.lift_var [definition, in nbe]
L.lift_var_empty [lemma, in nbe]
L.mult_subst [definition, in nbe]
L.mult_subst_app [lemma, in nbe]
L.mult_subst_comm [lemma, in nbe]
L.mult_subst_comma_first [lemma, in nbe]
L.mult_subst_lam [lemma, in nbe]
L.mult_subst_lift [lemma, in nbe]
L.mult_subst_lift_stmt [definition, in nbe]
L.neutral [inductive, in nbe]
L.neutral_app [constructor, in nbe]
L.neutral_rel [constructor, in nbe]
L.neutral_SCN [lemma, in nbe]
L.neutral_term [definition, in nbe]
L.next [constructor, in nbe]
L.nf [inductive, in nbe]
L.nf_cst [constructor, in nbe]
L.nf_lam [constructor, in nbe]
L.nf_neutral [constructor, in nbe]
L.nf_term [definition, in nbe]
L.nil_valuation [definition, in nbe]
L.normalizes [inductive, in nbe]
L.normalizes_app [inductive, in nbe]
L.normalizes_exp_stmt [lemma, in nbe]
L.normalizes_subst [lemma, in nbe]
L.normalizes_subst_stmt [definition, in nbe]
L.normalize_app_det [lemma, in nbe]
L.normalize_complete [lemma, in nbe]
L.normalize_correct [lemma, in nbe]
L.normalize_det [lemma, in nbe]
L.normalize_term_correct [lemma, in nbe]
L.normalize_term_det [lemma, in nbe]
L.norm_app [constructor, in nbe]
L.norm_app_app [constructor, in nbe]
L.norm_app_lam [constructor, in nbe]
L.norm_app_rel [constructor, in nbe]
L.norm_cst [constructor, in nbe]
L.norm_lam [constructor, in nbe]
L.norm_rel [constructor, in nbe]
L.R [definition, in nbe]
L.reduces [inductive, in nbe]
L.red_app [constructor, in nbe]
L.red_beta [constructor, in nbe]
L.red_R_R [lemma, in nbe]
L.red_SN_SN [lemma, in nbe]
L.rel [constructor, in nbe]
L.R_eval [lemma, in nbe]
L.R_substitutive [lemma, in nbe]
L.SCN [definition, in nbe]
L.SCN_neutral [definition, in nbe]
L.SCN_prop [definition, in nbe]
L.SCN_subst [lemma, in nbe]
L.SCN_subst_stmt [definition, in nbe]
L.SCons [constructor, in nbe]
L.SN [definition, in nbe]
L.SN [definition, in nbe]
L.SNil [constructor, in nbe]
L.SN_eval [lemma, in nbe]
L.SN_rel [lemma, in nbe]
L.SN_substitutive [lemma, in nbe]
L.SN_substitutive [lemma, in nbe]
L.SN_substitutive [lemma, in nbe]
L.SN_substitutive_stmt [definition, in nbe]
L.SN_substitutive_stmt [definition, in nbe]
L.strong_computability [lemma, in nbe]
L.strong_normalization_app [lemma, in nbe]
L.strong_normalization_app_stmt [definition, in nbe]
L.subst [definition, in nbe]
L.substitution [inductive, in nbe]
L.substitution_cons [lemma, in nbe]
L.substitution_cons_aux [lemma, in nbe]
L.substitution_R [definition, in nbe]
L.substitution_SN [definition, in nbe]
L.substitution_SN [definition, in nbe]
L.subst_comm [lemma, in nbe]
L.subst_cst [lemma, in nbe]
L.subst_lift [lemma, in nbe]
L.subst_lift [lemma, in nbe]
L.subst_lift_comm_full [lemma, in nbe]
L.subst_lift_comm_stmt [definition, in nbe]
L.subst_lift_rec [lemma, in nbe]
L.subst_lift_rec_stmt [definition, in nbe]
L.subst_lift_var [lemma, in nbe]
L.subst_lift_var_comm_stmt [definition, in nbe]
L.subst_rec [definition, in nbe]
L.subst_rec_comm [lemma, in nbe]
L.subst_rec_comma_first [lemma, in nbe]
L.subst_rec_comma_next [lemma, in nbe]
L.subst_rec_comm_stmt [definition, in nbe]
L.subst_rec_empty_first [lemma, in nbe]
L.subst_rec_empty_next [lemma, in nbe]
L.subst_var [definition, in nbe]
L.subst_var_rec [definition, in nbe]
L.subst_var_rec_comma_first [lemma, in nbe]
L.subst_var_rec_comma_next [lemma, in nbe]
L.subst_var_rec_empty_first [lemma, in nbe]
L.subst_var_rec_empty_next [lemma, in nbe]
L.term [inductive, in nbe]
L.term_wn [lemma, in nbe]
L.term_wn [lemma, in nbe]
L.type [inductive, in nbe]
L.type_arrow [constructor, in nbe]
L.type_cst [constructor, in nbe]
L.valuation [definition, in nbe]
L.var [inductive, in nbe]
L.var_case [lemma, in nbe]
L.var_case_aux [lemma, in nbe]

N

nat_id_term [definition, in nbe]
nat_type [definition, in nbe]
nbe [library]

T

type_constant [axiom, in nbe]
type_constants [definition, in nbe]

Axiom Index

C

constants [in nbe]
constant_types [in nbe]

T

type_constant [in nbe]

Lemma Index

L

L.app_assoc [in nbe]
L.app_empty [in nbe]
L.coerce_term_context_id [in nbe]
L.coerce_term_context_lift_rec [in nbe]
L.coerce_term_context_lift_rec_aux [in nbe]
L.coerce_var_context_id [in nbe]
L.coerce_var_context_lift_var [in nbe]
L.eq_rect_coerce [in nbe]
L.eq_rect_coerce_var [in nbe]
L.lift_lift [in nbe]
L.lift_lift_var [in nbe]
L.lift_rec_comma_first [in nbe]
L.lift_rec_comma_next [in nbe]
L.lift_rec_empty [in nbe]
L.lift_var_empty [in nbe]
L.mult_subst_app [in nbe]
L.mult_subst_comm [in nbe]
L.mult_subst_comma_first [in nbe]
L.mult_subst_lam [in nbe]
L.mult_subst_lift [in nbe]
L.neutral_SCN [in nbe]
L.normalizes_exp_stmt [in nbe]
L.normalizes_subst [in nbe]
L.normalize_app_det [in nbe]
L.normalize_complete [in nbe]
L.normalize_correct [in nbe]
L.normalize_det [in nbe]
L.normalize_term_correct [in nbe]
L.normalize_term_det [in nbe]
L.red_R_R [in nbe]
L.red_SN_SN [in nbe]
L.R_eval [in nbe]
L.R_substitutive [in nbe]
L.SCN_subst [in nbe]
L.SN_eval [in nbe]
L.SN_rel [in nbe]
L.SN_substitutive [in nbe]
L.SN_substitutive [in nbe]
L.SN_substitutive [in nbe]
L.strong_computability [in nbe]
L.strong_normalization_app [in nbe]
L.substitution_cons [in nbe]
L.substitution_cons_aux [in nbe]
L.subst_comm [in nbe]
L.subst_cst [in nbe]
L.subst_lift [in nbe]
L.subst_lift [in nbe]
L.subst_lift_comm_full [in nbe]
L.subst_lift_rec [in nbe]
L.subst_lift_var [in nbe]
L.subst_rec_comm [in nbe]
L.subst_rec_comma_first [in nbe]
L.subst_rec_comma_next [in nbe]
L.subst_rec_empty_first [in nbe]
L.subst_rec_empty_next [in nbe]
L.subst_var_rec_comma_first [in nbe]
L.subst_var_rec_comma_next [in nbe]
L.subst_var_rec_empty_first [in nbe]
L.subst_var_rec_empty_next [in nbe]
L.term_wn [in nbe]
L.term_wn [in nbe]
L.var_case [in nbe]
L.var_case_aux [in nbe]

Constructor Index

C

cst_bool [in nbe]
cst_bool_t [in nbe]
cst_nat [in nbe]
cst_nat_t [in nbe]

L

L.app [in nbe]
L.comma [in nbe]
L.conv_app [in nbe]
L.conv_lam [in nbe]
L.conv_red [in nbe]
L.conv_refl [in nbe]
L.conv_sym [in nbe]
L.conv_trans [in nbe]
L.cst [in nbe]
L.empty [in nbe]
L.eval_cst [in nbe]
L.eval_lam [in nbe]
L.eval_trans [in nbe]
L.first [in nbe]
L.lam [in nbe]
L.neutral_app [in nbe]
L.neutral_rel [in nbe]
L.next [in nbe]
L.nf_cst [in nbe]
L.nf_lam [in nbe]
L.nf_neutral [in nbe]
L.norm_app [in nbe]
L.norm_app_app [in nbe]
L.norm_app_lam [in nbe]
L.norm_app_rel [in nbe]
L.norm_cst [in nbe]
L.norm_lam [in nbe]
L.norm_rel [in nbe]
L.red_app [in nbe]
L.red_beta [in nbe]
L.rel [in nbe]
L.SCons [in nbe]
L.SNil [in nbe]
L.type_arrow [in nbe]
L.type_cst [in nbe]

Inductive Index

C

csts [in nbe]
cst_types [in nbe]

L

L.conv [in nbe]
L.ctx [in nbe]
L.evaluates [in nbe]
L.neutral [in nbe]
L.nf [in nbe]
L.normalizes [in nbe]
L.normalizes_app [in nbe]
L.reduces [in nbe]
L.substitution [in nbe]
L.term [in nbe]
L.type [in nbe]
L.var [in nbe]

Definition Index

C

C.constants [in nbe]
C.constant_types [in nbe]
C.type_constant [in nbe]

I

interp_closed_nb [in nbe]
interp_constant [in nbe]
interp_constant_type [in nbe]
interp_nb [in nbe]
interp_nb_type [in nbe]

L

L.append [in nbe]
L.augment_valuation [in nbe]
L.coerce_neutral_context [in nbe]
L.coerce_nf_context [in nbe]
L.coerce_subst_context [in nbe]
L.coerce_term_context [in nbe]
L.coerce_var_context [in nbe]
L.interp_closed_term [in nbe]
L.interp_term [in nbe]
L.interp_type [in nbe]
L.is_normalizing [in nbe]
L.is_normalizing_app [in nbe]
L.lift [in nbe]
L.lift_ctx [in nbe]
L.lift_lift_stmt [in nbe]
L.lift_lift_var_stmt [in nbe]
L.lift_rec [in nbe]
L.lift_var [in nbe]
L.mult_subst [in nbe]
L.mult_subst_lift_stmt [in nbe]
L.neutral_term [in nbe]
L.nf_term [in nbe]
L.nil_valuation [in nbe]
L.normalizes_subst_stmt [in nbe]
L.R [in nbe]
L.SCN [in nbe]
L.SCN_neutral [in nbe]
L.SCN_prop [in nbe]
L.SCN_subst_stmt [in nbe]
L.SN [in nbe]
L.SN [in nbe]
L.SN_substitutive_stmt [in nbe]
L.SN_substitutive_stmt [in nbe]
L.strong_normalization_app_stmt [in nbe]
L.subst [in nbe]
L.substitution_R [in nbe]
L.substitution_SN [in nbe]
L.substitution_SN [in nbe]
L.subst_lift_comm_stmt [in nbe]
L.subst_lift_rec_stmt [in nbe]
L.subst_lift_var_comm_stmt [in nbe]
L.subst_rec [in nbe]
L.subst_rec_comm_stmt [in nbe]
L.subst_var [in nbe]
L.subst_var_rec [in nbe]
L.valuation [in nbe]

N

nat_id_term [in nbe]
nat_type [in nbe]

T

type_constants [in nbe]

Module Index

C

C [in nbe]
Constants [in nbe]

L

L [in nbe]

Library Index

N

nbe

Global Index

A

B

D

E

F

G

H

J

K

M

O

P

Q

R

S

U

V

W

X

Y

Z

_

(180 entries)

Axiom Index

A

B

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

U

V

W

X

Y

Z

_

(3 entries)

Lemma Index

A

B

C

D

E

F

G

H

I

J

K

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(63 entries)

Constructor Index

A

B

D

E

F

G

H

I

J

K

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(39 entries)

Inductive Index

A

B

D

E

F

G

H

I

J

K

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(14 entries)

Definition Index

A

B

D

E

F

G

H

J

K

M

O

P

Q

R

S

U

V

W

X

Y

Z

_

(57 entries)

Module Index

A

B

D

E

F

G

H

I

J

K

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(3 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

L

M

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(1 entry)

This page has been generated by coqdoc