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 _ (329 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 _ (9 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 _ (137 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 _ (97 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 _ (38 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 _ (42 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 _ (6 entries)

Global Index

A

App [constructor, in compilation]
App [constructor, in semantics]
append_assoc [lemma, in traces]
append_trace_traceinf [definition, in traces]


B

Bottom [constructor, in densem]


C

Clos [constructor, in compilation]
closed [definition, in cps]
closed_App_inv [lemma, in cps]
closed_eval [lemma, in cps]
closed_subst [lemma, in cps]
code [definition, in compilation]
coeval [inductive, in compilation]
coeval [inductive, in semantics]
coeval_app [constructor, in semantics]
coeval_App [constructor, in compilation]
coeval_app_inv [lemma, in typing]
coeval_Const [constructor, in compilation]
coeval_const [constructor, in semantics]
coeval_const_inv [lemma, in typing]
coeval_cored [lemma, in semantics]
coeval_cps_characterization [lemma, in cps]
coeval_eval_or_evalinf [lemma, in semantics]
coeval_filinski_aux [lemma, in typing]
coeval_fun [constructor, in semantics]
coeval_Fun [constructor, in compilation]
coeval_fun_inv1 [lemma, in typing]
coeval_fun_inv2 [lemma, in typing]
coeval_noteval_evalinf [lemma, in semantics]
coeval_omega [lemma, in semantics]
coeval_value [lemma, in semantics]
coeval_value_or_red1 [lemma, in semantics]
coeval_Var [constructor, in compilation]
coeval_zerofun_omega [lemma, in semantics]
compilation [library]
compile [definition, in compilation]
compile_coeval [lemma, in compilation]
compile_coeval_aux [lemma, in compilation]
compile_env [definition, in compilation]
compile_eval [lemma, in compilation]
compile_evalinf [lemma, in compilation]
compile_evalinf_aux [lemma, in compilation]
compile_value [definition, in compilation]
compute [definition, in densem]
compute_converges [lemma, in densem]
compute_diverges [lemma, in densem]
compute_gets_stuck [lemma, in densem]
compute_increasing [lemma, in densem]
const [axiom, in semantics]
const [axiom, in compilation]
Const [constructor, in compilation]
Const [constructor, in semantics]
cons_right [definition, in traces]
cons_right_app [lemma, in traces]
converges_eval [lemma, in densem]
cored [inductive, in semantics]
cored_notred_redinf [lemma, in semantics]
cored_red_or_redinf [lemma, in semantics]
cored_refl [constructor, in semantics]
cored_step [constructor, in semantics]
cored_trans [lemma, in semantics]
cotrans [inductive, in compilation]
cotransN [inductive, in compilation]
cotransN_cotrans [lemma, in compilation]
cotransN_perform [constructor, in compilation]
cotransN_trans [constructor, in compilation]
cotrans_refl [constructor, in compilation]
cotrans_step [constructor, in compilation]
cps [library]


D

decompose_cotransN [lemma, in compilation]
decompose_traceinf [lemma, in traces]
decompose_transinfN [lemma, in compilation]
delta [definition, in traces]
delta [definition, in semantics]
densem [library]
diverges_evalinf [lemma, in densem]


E

env [definition, in compilation]
env_empty [axiom, in typing]
env_exten [axiom, in typing]
env_get [axiom, in typing]
env_get_empty [axiom, in typing]
env_get_set [axiom, in typing]
env_get_set_other [lemma, in typing]
env_get_set_same [lemma, in typing]
env_set [axiom, in typing]
Error [constructor, in densem]
eval [inductive, in semantics]
eval [inductive, in compilation]
evalinf [inductive, in semantics]
evalinf [inductive, in compilation]
evalinf_App_f [constructor, in compilation]
evalinf_app_f [constructor, in semantics]
evalinf_app_l [constructor, in semantics]
evalinf_App_l [constructor, in compilation]
evalinf_app_r [constructor, in semantics]
evalinf_App_r [constructor, in compilation]
evalinf_coeval_cps [lemma, in cps]
evalinf_diverges [lemma, in densem]
evalinf_omega [lemma, in semantics]
evalinf_omega_1 [definition, in semantics]
evalinf_progress [lemma, in typing]
evalinf_redinf [lemma, in semantics]
evalinf_red1 [lemma, in semantics]
evaluates [definition, in densem]
evaluates_compute_either [lemma, in densem]
evaluates_limsup [lemma, in densem]
evaluates_total [lemma, in densem]
evaluates_unique [lemma, in densem]
eval_app [constructor, in semantics]
eval_App [constructor, in compilation]
eval_atom [lemma, in cps]
eval_atom_inv [lemma, in cps]
eval_body_atom [lemma, in cps]
eval_body_fun [lemma, in cps]
eval_coeval [lemma, in semantics]
eval_coeval_deterministic [lemma, in semantics]
eval_const [constructor, in semantics]
eval_Const [constructor, in compilation]
eval_converges [lemma, in densem]
eval_deterministic [lemma, in semantics]
eval_evalinf_exclusive [lemma, in semantics]
eval_Fun [constructor, in compilation]
eval_fun [constructor, in semantics]
eval_isvalue [lemma, in semantics]
eval_or_not_eval [lemma, in typing]
eval_preservation [lemma, in typing]
eval_red [lemma, in semantics]
eval_value [lemma, in semantics]
eval_Var [constructor, in compilation]


F

filinski [definition, in typing]
filinski1 [definition, in typing]
filinski2 [definition, in typing]
find_var_match [lemma, in compilation]
Fun [constructor, in semantics]
Fun [constructor, in compilation]


H

has_type [inductive, in typing]
has_type_app [constructor, in typing]
has_type_const [constructor, in typing]
has_type_fun [constructor, in typing]
has_type_subst [lemma, in typing]
has_type_var [constructor, in typing]
has_type_weaken [lemma, in typing]
height_term [definition, in typing]


I

IApp [constructor, in compilation]
IClosure [constructor, in compilation]
IConst [constructor, in compilation]
infinite_progress_redinf [lemma, in semantics]
INop [constructor, in compilation]
instr [inductive, in compilation]
Int [constructor, in compilation]
IReturn [constructor, in compilation]
isatom [inductive, in cps]
isatom_const [constructor, in cps]
isatom_fun [constructor, in cps]
isatom_var [constructor, in cps]
isbody [inductive, in cps]
isbody_app [constructor, in cps]
isbody_atom [constructor, in cps]
isbody_subst [lemma, in cps]
isfree [definition, in cps]
isfree_subst [lemma, in cps]
isvalue [inductive, in semantics]
isvalue_const [constructor, in semantics]
isvalue_dec [lemma, in traces]
isvalue_fun [constructor, in semantics]
isvalue_reduce1 [lemma, in traces]
IVar [constructor, in compilation]


L

left_app_height [definition, in compilation]


M

MClos [constructor, in compilation]
menv [definition, in compilation]
MInt [constructor, in compilation]
mvalue [inductive, in compilation]


N

notred [definition, in semantics]
not_coeval_filinski [lemma, in typing]
not_cored_coeval [lemma, in semantics]
not_evalinf_atom [lemma, in cps]
not_evalinf_coeval [lemma, in semantics]
not_eval_omega [lemma, in semantics]
not_eval_omega [lemma, in traces]


O

Omega [definition, in cps]
omega [definition, in semantics]
omega [definition, in traces]
omegatrace [definition, in traces]


R

red [inductive, in semantics]
redinf [inductive, in semantics]
redinf_app_l [lemma, in semantics]
redinf_app_r [lemma, in semantics]
redinf_cored [lemma, in semantics]
redinf_evalinf [lemma, in traces]
redinf_evalinf [lemma, in semantics]
redinf_intro [constructor, in semantics]
redinf_tredinf_aux [lemma, in traces]
reduce1 [definition, in traces]
red1 [inductive, in semantics]
red1_app_l [constructor, in semantics]
red1_app_r [constructor, in semantics]
red1_beta [constructor, in semantics]
red1_deterministic [lemma, in semantics]
red1_eval [lemma, in semantics]
red1_preservation [lemma, in typing]
red1_progress [lemma, in typing]
red1_reduce1 [lemma, in traces]
red_app_l [lemma, in semantics]
red_app_r [lemma, in semantics]
red_cored [lemma, in semantics]
red_eval [lemma, in semantics]
red_one [lemma, in semantics]
red_or_redinf [lemma, in semantics]
red_preservation [lemma, in typing]
red_refl [constructor, in semantics]
red_step [constructor, in semantics]
red_trans [lemma, in semantics]
red_tred [lemma, in traces]
result [inductive, in densem]
Result [constructor, in densem]
result_le [inductive, in densem]
result_le_bot [constructor, in densem]
result_le_refl [constructor, in densem]


S

safered [inductive, in typing]
safered_step [constructor, in typing]
safered_value [constructor, in typing]
semantics [library]
slot [inductive, in compilation]
Slot_return [constructor, in compilation]
Slot_value [constructor, in compilation]
soundness1 [lemma, in typing]
soundness2 [lemma, in typing]
soundness3 [lemma, in typing]
soundness4 [lemma, in typing]
soundness5 [lemma, in typing]
stack [definition, in compilation]
step [definition, in densem]
step_increasing [lemma, in densem]
subst [definition, in semantics]


T

Tarrow [constructor, in typing]
Tcons [constructor, in traces]
term [inductive, in semantics]
term [inductive, in compilation]
teval [inductive, in traces]
tevalinf [inductive, in traces]
tevalinf_app_f [constructor, in traces]
tevalinf_app_l [constructor, in traces]
tevalinf_app_r [constructor, in traces]
tevalinf_deterministic [lemma, in traces]
tevalinf_omega [lemma, in traces]
tevalinf_tredinf [lemma, in traces]
tevalinf_tredinf' [lemma, in traces]
tevalinf_tred1 [lemma, in traces]
teval_app [constructor, in traces]
teval_const [constructor, in traces]
teval_deterministic [lemma, in traces]
teval_fun [constructor, in traces]
teval_isvalue [lemma, in traces]
teval_tred [lemma, in traces]
teval_value [lemma, in traces]
Tint [constructor, in typing]
trace [definition, in traces]
traceinf [inductive, in traces]
traceinf_app_l [definition, in traces]
traceinf_app_r [definition, in traces]
traceinf_for [definition, in traces]
traceinf_sim [inductive, in traces]
traceinf_sim_intro [constructor, in traces]
traceinf_sim_refl [lemma, in traces]
traceinf_sim_sym [lemma, in traces]
traceinf_sim_trans [lemma, in traces]
traces [library]
trace_app_l [definition, in traces]
trace_app_r [definition, in traces]
trans [inductive, in compilation]
transinf [inductive, in compilation]
transinfN [inductive, in compilation]
transinfN_perform [constructor, in compilation]
transinfN_stutter [constructor, in compilation]
transinfN_transinf [lemma, in compilation]
transinf_intro [constructor, in compilation]
transition [inductive, in compilation]
transplus [inductive, in compilation]
transplus_base [constructor, in compilation]
transplus_step [constructor, in compilation]
transplus_trans [lemma, in compilation]
transplus_transitive [lemma, in compilation]
trans_IApp [constructor, in compilation]
trans_IClosure [constructor, in compilation]
trans_IConst [constructor, in compilation]
trans_INop [constructor, in compilation]
trans_IReturn [constructor, in compilation]
trans_IVar [constructor, in compilation]
trans_refl [constructor, in compilation]
trans_step [constructor, in compilation]
tred [inductive, in traces]
tredinf [inductive, in traces]
tredinf' [inductive, in traces]
tredinf'_intro [constructor, in traces]
tredinf'_tredinf [lemma, in traces]
tredinf_app_l [lemma, in traces]
tredinf_app_l_1 [lemma, in traces]
tredinf_app_l_2 [lemma, in traces]
tredinf_app_r [lemma, in traces]
tredinf_app_r_1 [lemma, in traces]
tredinf_app_r_2 [lemma, in traces]
tredinf_decompose [lemma, in traces]
tredinf_deterministic [lemma, in traces]
tredinf_intro [constructor, in traces]
tred1_teval [lemma, in traces]
tred_app_l [lemma, in traces]
tred_app_r [lemma, in traces]
tred_one [lemma, in traces]
tred_or_redinf [lemma, in traces]
tred_or_tredinf [lemma, in traces]
tred_red [lemma, in traces]
tred_refl [constructor, in traces]
tred_step [constructor, in traces]
tred_teval [lemma, in traces]
tred_trans [lemma, in traces]
type [inductive, in typing]
typenv [axiom, in typing]
typing [library]


V

value [inductive, in compilation]
value_notred [lemma, in semantics]
var [definition, in semantics]
Var [constructor, in semantics]
Var [constructor, in compilation]
var_eq [lemma, in semantics]
vf [definition, in typing]
vg [definition, in typing]
vx [definition, in traces]
vx [definition, in semantics]
vy [definition, in typing]


Y

Y [definition, in typing]



Axiom Index

C

const [in semantics]
const [in compilation]


E

env_empty [in typing]
env_exten [in typing]
env_get [in typing]
env_get_empty [in typing]
env_get_set [in typing]
env_set [in typing]


T

typenv [in typing]



Lemma Index

A

append_assoc [in traces]


C

closed_App_inv [in cps]
closed_eval [in cps]
closed_subst [in cps]
coeval_app_inv [in typing]
coeval_const_inv [in typing]
coeval_cored [in semantics]
coeval_cps_characterization [in cps]
coeval_eval_or_evalinf [in semantics]
coeval_filinski_aux [in typing]
coeval_fun_inv1 [in typing]
coeval_fun_inv2 [in typing]
coeval_noteval_evalinf [in semantics]
coeval_omega [in semantics]
coeval_value [in semantics]
coeval_value_or_red1 [in semantics]
coeval_zerofun_omega [in semantics]
compile_coeval [in compilation]
compile_coeval_aux [in compilation]
compile_eval [in compilation]
compile_evalinf [in compilation]
compile_evalinf_aux [in compilation]
compute_converges [in densem]
compute_diverges [in densem]
compute_gets_stuck [in densem]
compute_increasing [in densem]
cons_right_app [in traces]
converges_eval [in densem]
cored_notred_redinf [in semantics]
cored_red_or_redinf [in semantics]
cored_trans [in semantics]
cotransN_cotrans [in compilation]


D

decompose_cotransN [in compilation]
decompose_traceinf [in traces]
decompose_transinfN [in compilation]
diverges_evalinf [in densem]


E

env_get_set_other [in typing]
env_get_set_same [in typing]
evalinf_coeval_cps [in cps]
evalinf_diverges [in densem]
evalinf_omega [in semantics]
evalinf_progress [in typing]
evalinf_redinf [in semantics]
evalinf_red1 [in semantics]
evaluates_compute_either [in densem]
evaluates_limsup [in densem]
evaluates_total [in densem]
evaluates_unique [in densem]
eval_atom [in cps]
eval_atom_inv [in cps]
eval_body_atom [in cps]
eval_body_fun [in cps]
eval_coeval [in semantics]
eval_coeval_deterministic [in semantics]
eval_converges [in densem]
eval_deterministic [in semantics]
eval_evalinf_exclusive [in semantics]
eval_isvalue [in semantics]
eval_or_not_eval [in typing]
eval_preservation [in typing]
eval_red [in semantics]
eval_value [in semantics]


F

find_var_match [in compilation]


H

has_type_subst [in typing]
has_type_weaken [in typing]


I

infinite_progress_redinf [in semantics]
isbody_subst [in cps]
isfree_subst [in cps]
isvalue_dec [in traces]
isvalue_reduce1 [in traces]


N

not_coeval_filinski [in typing]
not_cored_coeval [in semantics]
not_evalinf_atom [in cps]
not_evalinf_coeval [in semantics]
not_eval_omega [in semantics]
not_eval_omega [in traces]


R

redinf_app_l [in semantics]
redinf_app_r [in semantics]
redinf_cored [in semantics]
redinf_evalinf [in traces]
redinf_evalinf [in semantics]
redinf_tredinf_aux [in traces]
red1_deterministic [in semantics]
red1_eval [in semantics]
red1_preservation [in typing]
red1_progress [in typing]
red1_reduce1 [in traces]
red_app_l [in semantics]
red_app_r [in semantics]
red_cored [in semantics]
red_eval [in semantics]
red_one [in semantics]
red_or_redinf [in semantics]
red_preservation [in typing]
red_trans [in semantics]
red_tred [in traces]


S

soundness1 [in typing]
soundness2 [in typing]
soundness3 [in typing]
soundness4 [in typing]
soundness5 [in typing]
step_increasing [in densem]


T

tevalinf_deterministic [in traces]
tevalinf_omega [in traces]
tevalinf_tredinf [in traces]
tevalinf_tredinf' [in traces]
tevalinf_tred1 [in traces]
teval_deterministic [in traces]
teval_isvalue [in traces]
teval_tred [in traces]
teval_value [in traces]
traceinf_sim_refl [in traces]
traceinf_sim_sym [in traces]
traceinf_sim_trans [in traces]
transinfN_transinf [in compilation]
transplus_trans [in compilation]
transplus_transitive [in compilation]
tredinf'_tredinf [in traces]
tredinf_app_l [in traces]
tredinf_app_l_1 [in traces]
tredinf_app_l_2 [in traces]
tredinf_app_r [in traces]
tredinf_app_r_1 [in traces]
tredinf_app_r_2 [in traces]
tredinf_decompose [in traces]
tredinf_deterministic [in traces]
tred1_teval [in traces]
tred_app_l [in traces]
tred_app_r [in traces]
tred_one [in traces]
tred_or_redinf [in traces]
tred_or_tredinf [in traces]
tred_red [in traces]
tred_teval [in traces]
tred_trans [in traces]


V

value_notred [in semantics]
var_eq [in semantics]



Constructor Index

A

App [in compilation]
App [in semantics]


B

Bottom [in densem]


C

Clos [in compilation]
coeval_app [in semantics]
coeval_App [in compilation]
coeval_Const [in compilation]
coeval_const [in semantics]
coeval_fun [in semantics]
coeval_Fun [in compilation]
coeval_Var [in compilation]
Const [in compilation]
Const [in semantics]
cored_refl [in semantics]
cored_step [in semantics]
cotransN_perform [in compilation]
cotransN_trans [in compilation]
cotrans_refl [in compilation]
cotrans_step [in compilation]


E

Error [in densem]
evalinf_App_f [in compilation]
evalinf_app_f [in semantics]
evalinf_app_l [in semantics]
evalinf_App_l [in compilation]
evalinf_app_r [in semantics]
evalinf_App_r [in compilation]
eval_app [in semantics]
eval_App [in compilation]
eval_const [in semantics]
eval_Const [in compilation]
eval_Fun [in compilation]
eval_fun [in semantics]
eval_Var [in compilation]


F

Fun [in semantics]
Fun [in compilation]


H

has_type_app [in typing]
has_type_const [in typing]
has_type_fun [in typing]
has_type_var [in typing]


I

IApp [in compilation]
IClosure [in compilation]
IConst [in compilation]
INop [in compilation]
Int [in compilation]
IReturn [in compilation]
isatom_const [in cps]
isatom_fun [in cps]
isatom_var [in cps]
isbody_app [in cps]
isbody_atom [in cps]
isvalue_const [in semantics]
isvalue_fun [in semantics]
IVar [in compilation]


M

MClos [in compilation]
MInt [in compilation]


R

redinf_intro [in semantics]
red1_app_l [in semantics]
red1_app_r [in semantics]
red1_beta [in semantics]
red_refl [in semantics]
red_step [in semantics]
Result [in densem]
result_le_bot [in densem]
result_le_refl [in densem]


S

safered_step [in typing]
safered_value [in typing]
Slot_return [in compilation]
Slot_value [in compilation]


T

Tarrow [in typing]
Tcons [in traces]
tevalinf_app_f [in traces]
tevalinf_app_l [in traces]
tevalinf_app_r [in traces]
teval_app [in traces]
teval_const [in traces]
teval_fun [in traces]
Tint [in typing]
traceinf_sim_intro [in traces]
transinfN_perform [in compilation]
transinfN_stutter [in compilation]
transinf_intro [in compilation]
transplus_base [in compilation]
transplus_step [in compilation]
trans_IApp [in compilation]
trans_IClosure [in compilation]
trans_IConst [in compilation]
trans_INop [in compilation]
trans_IReturn [in compilation]
trans_IVar [in compilation]
trans_refl [in compilation]
trans_step [in compilation]
tredinf'_intro [in traces]
tredinf_intro [in traces]
tred_refl [in traces]
tred_step [in traces]


V

Var [in semantics]
Var [in compilation]



Inductive Index

C

coeval [in compilation]
coeval [in semantics]
cored [in semantics]
cotrans [in compilation]
cotransN [in compilation]


E

eval [in semantics]
eval [in compilation]
evalinf [in semantics]
evalinf [in compilation]


H

has_type [in typing]


I

instr [in compilation]
isatom [in cps]
isbody [in cps]
isvalue [in semantics]


M

mvalue [in compilation]


R

red [in semantics]
redinf [in semantics]
red1 [in semantics]
result [in densem]
result_le [in densem]


S

safered [in typing]
slot [in compilation]


T

term [in semantics]
term [in compilation]
teval [in traces]
tevalinf [in traces]
traceinf [in traces]
traceinf_sim [in traces]
trans [in compilation]
transinf [in compilation]
transinfN [in compilation]
transition [in compilation]
transplus [in compilation]
tred [in traces]
tredinf [in traces]
tredinf' [in traces]
type [in typing]


V

value [in compilation]



Definition Index

A

append_trace_traceinf [in traces]


C

closed [in cps]
code [in compilation]
compile [in compilation]
compile_env [in compilation]
compile_value [in compilation]
compute [in densem]
cons_right [in traces]


D

delta [in traces]
delta [in semantics]


E

env [in compilation]
evalinf_omega_1 [in semantics]
evaluates [in densem]


F

filinski [in typing]
filinski1 [in typing]
filinski2 [in typing]


H

height_term [in typing]


I

isfree [in cps]


L

left_app_height [in compilation]


M

menv [in compilation]


N

notred [in semantics]


O

Omega [in cps]
omega [in semantics]
omega [in traces]
omegatrace [in traces]


R

reduce1 [in traces]


S

stack [in compilation]
step [in densem]
subst [in semantics]


T

trace [in traces]
traceinf_app_l [in traces]
traceinf_app_r [in traces]
traceinf_for [in traces]
trace_app_l [in traces]
trace_app_r [in traces]


V

var [in semantics]
vf [in typing]
vg [in typing]
vx [in traces]
vx [in semantics]
vy [in typing]


Y

Y [in typing]



Library Index

C

compilation
cps


D

densem


S

semantics


T

traces
typing



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 _ (329 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 _ (9 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 _ (137 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 _ (97 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 _ (38 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 _ (42 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 _ (6 entries)

This page has been generated by coqdoc