| 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 | (370 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 | (144 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 | (1 entry) |
| 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 | (15 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 | (121 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 | (22 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 | (57 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 | (5 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 | (5 entries) |
Global Index
A
allowed_taskid_upd [lemma, in proofs]allowed_taskid [definition, in proofs]
appctx_context_exp [definition, in lang]
app_stack_app [lemma, in proofs]
app_stack1 [lemma, in proofs]
app_stack [definition, in proofs]
B
basis [library]branch [inductive, in lang]
B_finished [constructor, in lang]
B_right [constructor, in lang]
B_left [constructor, in lang]
B_neither [constructor, in lang]
C
cexp_rel_right_mult [lemma, in proofs]cexp_rel_preserve [lemma, in proofs]
cexp_rel_right_det [lemma, in proofs]
cexp_rel_left_det [lemma, in proofs]
cexp_rel_ind [definition, in proofs]
cexp_rel_right_ind1 [definition, in proofs]
cexp_rel_left_ind1 [definition, in proofs]
cexp_rel_right_Right [constructor, in proofs]
cexp_rel_right_Left [constructor, in proofs]
cexp_rel_right_Neither [constructor, in proofs]
cexp_rel_right_Finished [constructor, in proofs]
cexp_rel_right_Fail [constructor, in proofs]
cexp_rel_right_Run [constructor, in proofs]
cexp_rel_right_Start [constructor, in proofs]
cexp_rel_right_Thunk [constructor, in proofs]
cexp_rel_right [inductive, in proofs]
cexp_rel_left_Right [constructor, in proofs]
cexp_rel_left_Left [constructor, in proofs]
cexp_rel_left_Neither [constructor, in proofs]
cexp_rel_left_Finished [constructor, in proofs]
cexp_rel_left_Fail [constructor, in proofs]
cexp_rel_left_Run [constructor, in proofs]
cexp_rel_left_Start [constructor, in proofs]
cexp_rel_left [inductive, in proofs]
combine_results [library]
Completeness [lemma, in proofs]
completeness_one_step [lemma, in proofs]
completeness_ss [lemma, in proofs]
context [inductive, in lang]
Correctness [lemma, in proofs]
count [definition, in proofs]
count_empty [lemma, in proofs]
count_nonneg [lemma, in proofs]
count_list_deque [lemma, in proofs]
count_list_stack [lemma, in proofs]
count_list_app [lemma, in proofs]
count_list [definition, in proofs]
count_update [lemma, in proofs]
count_rec_upd [lemma, in proofs]
count_split [lemma, in proofs]
count_helper [lemma, in proofs]
count_rec [definition, in proofs]
count1 [lemma, in proofs]
count1_int [lemma, in proofs]
count2 [lemma, in proofs]
C_letL [constructor, in lang]
C_pairR [constructor, in lang]
C_pairL [constructor, in lang]
D
deque [definition, in lang]deque_taskids_app [lemma, in proofs]
deque_taskids [definition, in proofs]
E
Eapp [constructor, in lang]Efst [constructor, in lang]
Eifnz [constructor, in lang]
Elet [constructor, in lang]
empty_map [definition, in lang]
Epair [constructor, in lang]
Eplus [constructor, in lang]
eq_termvar [lemma, in lang]
Esnd [constructor, in lang]
Eval [constructor, in lang]
exp [inductive, in lang]
exp_not_value [definition, in lang]
exp_app_app [lemma, in proofs]
exp_app [definition, in proofs]
F
fail_step [lemma, in proofs]ffun [definition, in lang]
ff_update [definition, in lang]
ff_deterministic [lemma, in proofs]
finished_stable [lemma, in proofs]
fp_deterministic [lemma, in proofs]
fp_recover_transitivity [lemma, in proofs]
fp_implies_ff [lemma, in proofs]
G
geq [inductive, in proofs]geq_transitive [lemma, in proofs]
geq_impl_pseq [lemma, in proofs]
geq_reflexive [lemma, in proofs]
Geq_letr2 [constructor, in proofs]
Geq_letr1 [constructor, in proofs]
Geq_letl [constructor, in proofs]
Geq_Ptuple [constructor, in proofs]
Geq_Val [constructor, in proofs]
Geq_Bot [constructor, in proofs]
I
identifier [definition, in lang]indeq_step [lemma, in proofs]
in_list_minus2 [lemma, in basis]
in_list_minus2I [lemma, in basis]
in_list_minus [lemma, in basis]
in_list_minusI [lemma, in basis]
in_map_fst [lemma, in basis]
In_right_deq [lemma, in proofs]
in_count [lemma, in proofs]
is_zero [definition, in lang]
is_true [definition, in Vtac]
L
lang [library]letFirst [lemma, in proofs]
ListDefs [section, in basis]
ListDefs.A [variable, in basis]
ListDefs.B [variable, in basis]
ListDefs.C [variable, in basis]
ListDefs.D [variable, in basis]
ListDefs.myeq [variable, in basis]
list_disj_minus2_mon [lemma, in basis]
list_disj_map_fst_minus2 [lemma, in basis]
list_assoc_flip [lemma, in basis]
list_disj_spec [lemma, in basis]
list_disj_mon_r [lemma, in basis]
list_disj_mon_l [lemma, in basis]
list_disj_minus_r [lemma, in basis]
list_disj_minus_l [lemma, in basis]
list_disj_app_l [lemma, in basis]
list_disj_app_r [lemma, in basis]
list_disj_app_rD [lemma, in basis]
list_disj_app_rI [lemma, in basis]
list_disj_comm [lemma, in basis]
list_disj_cons_l [lemma, in basis]
list_minus2_eq [lemma, in basis]
list_map_fst_minus2 [lemma, in basis]
list_minus2_remdup2 [lemma, in basis]
list_minus2_comm [lemma, in basis]
list_minus2_app_r [lemma, in basis]
list_minus2_app [lemma, in basis]
list_minus_swap [lemma, in basis]
list_minus_red [lemma, in basis]
list_minus_map_fst [lemma, in basis]
list_minus_comm [lemma, in basis]
list_minus_app_r [lemma, in basis]
list_minus_app [lemma, in basis]
list_assoc_someD [lemma, in basis]
list_assoc_noneD [lemma, in basis]
list_assoc_spec [lemma, in basis]
list_assoc_remdup2 [lemma, in basis]
list_assoc_minus2 [lemma, in basis]
list_assoc_app [lemma, in basis]
list_mem_map_fst [lemma, in basis]
list_mem_eq [lemma, in basis]
list_mem_spec [lemma, in basis]
list_mem_remdup [lemma, in basis]
list_mem_minus [lemma, in basis]
list_mem_app [lemma, in basis]
list_remdup2 [definition, in basis]
list_remdup [definition, in basis]
list_disj [definition, in basis]
list_minus2 [definition, in basis]
list_minus [definition, in basis]
list_assoc [definition, in basis]
list_mem [definition, in basis]
list_sum_nonneg [lemma, in proofs]
list_sum_app [lemma, in proofs]
list_sum [definition, in proofs]
M
map_snd_map_pair [lemma, in basis]map_fst_map_pair [lemma, in basis]
map_pair [definition, in basis]
mp [lemma, in Vtac]
mpstep [inductive, in lang]
mpstep_right_last [constructor, in lang]
mpstep_right_first [constructor, in lang]
mpstep_left_last [constructor, in lang]
mpstep_left_first [constructor, in lang]
mpstep_pop_task [constructor, in lang]
mpstep_local [constructor, in lang]
mpstep_steal [constructor, in lang]
mpstep_recover [constructor, in lang]
mpstep_fork [constructor, in lang]
mpstep_completeness [lemma, in proofs]
mpstep_soundness [lemma, in proofs]
mpstep_right [lemma, in proofs]
mpstep_left [lemma, in proofs]
mpstep_neither [lemma, in proofs]
mpstep_star_trans [lemma, in proofs]
mpstep_star_one [lemma, in proofs]
mpstep_starT [constructor, in proofs]
mpstep_starR [constructor, in proofs]
mpstep_star [inductive, in proofs]
N
nat_eq [lemma, in proofs]NoDup_app [lemma, in proofs]
nodup_count [lemma, in proofs]
not_value [definition, in lang]
NW [definition, in Vtac]
P
pairFirst [lemma, in proofs]pairSecond [lemma, in proofs]
PCfail [constructor, in lang]
PCfinish [constructor, in lang]
PCrecover [constructor, in lang]
PCrun [constructor, in lang]
PCstart [constructor, in lang]
pidentifier [definition, in lang]
pm_istid_nonneg [lemma, in proofs]
pm_istid [definition, in proofs]
proc_map [definition, in lang]
proc_config [inductive, in lang]
Progress [lemma, in proofs]
proofs [library]
pseq [inductive, in proofs]
PSeq_letr2 [constructor, in proofs]
PSeq_letl [constructor, in proofs]
PSeq_Ptuple [constructor, in proofs]
PSeq_Val [constructor, in proofs]
PSeq_Bot [constructor, in proofs]
R
Rbot [constructor, in lang]recover [inductive, in lang]
recover_tuple [lemma, in lang]
recover_ptuple [constructor, in lang]
recover_letRF [constructor, in lang]
recover_letRS [constructor, in lang]
recover_letLFR [constructor, in lang]
recover_letLFL [constructor, in lang]
recover_letLS [constructor, in lang]
recover_bottom [constructor, in lang]
recover_init [constructor, in lang]
recover_implies_fp [lemma, in proofs]
recover_starT [constructor, in proofs]
recover_starR [constructor, in proofs]
recover_star [inductive, in proofs]
reduce [inductive, in lang]
reducef [inductive, in lang]
reducef_tuple [lemma, in lang]
reducef_letFR [constructor, in lang]
reducef_letFL [constructor, in lang]
reducef_bottom [constructor, in lang]
reducef_ptuple [constructor, in lang]
reducef_if_false [constructor, in lang]
reducef_if_true [constructor, in lang]
reducef_second [constructor, in lang]
reducef_first [constructor, in lang]
reducef_app [constructor, in lang]
reducef_let [constructor, in lang]
reducef_plus [constructor, in lang]
reducef_init [constructor, in lang]
reduce_ptuple [constructor, in lang]
reduce_if_false [constructor, in lang]
reduce_if_true [constructor, in lang]
reduce_second [constructor, in lang]
reduce_first [constructor, in lang]
reduce_app [constructor, in lang]
reduce_let [constructor, in lang]
reduce_plus [constructor, in lang]
reduce_init [constructor, in lang]
res [inductive, in lang]
result_map [definition, in lang]
res_combine_results [lemma, in combine_results]
res_combine_rletr [lemma, in combine_results]
res_combine_rletl [lemma, in combine_results]
res_combine_bot [lemma, in combine_results]
res_combine_ptuple [lemma, in combine_results]
res_combine_values [lemma, in combine_results]
res_combine [definition, in lang]
Rletl [constructor, in lang]
Rletr [constructor, in lang]
rm_istid_nonneg [lemma, in proofs]
rm_istid [definition, in proofs]
rm_taskids [definition, in proofs]
rm_run [lemma, in proofs]
rm_ru [lemma, in proofs]
rm_ruo [lemma, in proofs]
rm_rus [lemma, in proofs]
Rptuple [constructor, in lang]
run_step [lemma, in proofs]
Rval [constructor, in lang]
S
soundness_ss [lemma, in proofs]soundness_helper_ss [lemma, in proofs]
spstep [inductive, in lang]
spstep_fail [constructor, in lang]
spstep_apply_context [constructor, in lang]
spstep_push_context [constructor, in lang]
spstep_run [constructor, in lang]
spstep_eval [constructor, in lang]
ss_star_pair [lemma, in proofs]
ss_star_exp_app [lemma, in proofs]
ss_impl_mpstep_s_start [lemma, in proofs]
ss_impl_mpstep_s [lemma, in proofs]
ss_star_trans [lemma, in proofs]
ss_star_one [lemma, in proofs]
ss_starT [constructor, in proofs]
ss_starR [constructor, in proofs]
ss_star [inductive, in proofs]
stack [inductive, in lang]
stack_decomp [lemma, in proofs]
stack_last_app [lemma, in proofs]
stack_app_det_right [lemma, in proofs]
stack_app_det_left [lemma, in proofs]
stack_taskids_app [lemma, in proofs]
stack_istid_nonneg [lemma, in proofs]
stack_istid [definition, in proofs]
stack_taskids [definition, in proofs]
stack_conts [definition, in proofs]
stack_last [definition, in proofs]
stack_app [definition, in proofs]
start_step [lemma, in proofs]
step [inductive, in lang]
step_par_join [constructor, in lang]
step_par_right [constructor, in lang]
step_par_left [constructor, in lang]
step_ifnz_false [constructor, in lang]
step_ifnz_true [constructor, in lang]
step_second [constructor, in lang]
step_first [constructor, in lang]
step_app [constructor, in lang]
step_letII [constructor, in lang]
step_letI [constructor, in lang]
step_plus [constructor, in lang]
step_exp_app [lemma, in proofs]
step_app_stack [lemma, in proofs]
subst_proc_config [definition, in lang]
subst_branch [definition, in lang]
subst_res [definition, in lang]
subst_task [definition, in lang]
subst_stack [definition, in lang]
subst_context [definition, in lang]
subst_exp [definition, in lang]
subst_val [definition, in lang]
S_cons [constructor, in lang]
S_right [constructor, in lang]
S_left [constructor, in lang]
T
task [inductive, in lang]taskid [inductive, in lang]
taskids [definition, in proofs]
task_istid_nonneg [lemma, in proofs]
task_istid [definition, in proofs]
termvar [definition, in lang]
TIDleft [constructor, in lang]
TIDright [constructor, in lang]
tid_eq [definition, in proofs]
T_right [constructor, in lang]
V
val [inductive, in lang]Vfunc [constructor, in lang]
Vint [constructor, in lang]
vlib__andb_split [lemma, in Vtac]
vlib__negb_rewrite [lemma, in Vtac]
vlib__not_false_is_true [lemma, in Vtac]
vlib__true_is_true [lemma, in Vtac]
Vpair [constructor, in lang]
Vtac [library]
Vvar [constructor, in lang]
W
well_formed [definition, in proofs]well_formed_nd_alt [definition, in proofs]
well_formed_nd [definition, in proofs]
wf_preserved [lemma, in proofs]
wf_nd_altI [lemma, in proofs]
wf_prnd [lemma, in proofs]
wf_rrnd [lemma, in proofs]
wf_ppnd [lemma, in proofs]
wf_preserved_nd [lemma, in proofs]
other
_ # _ [notation, in combine_results]_ <12= _ [notation, in Vtac]
_ <11= _ [notation, in Vtac]
_ <10= _ [notation, in Vtac]
_ <9= _ [notation, in Vtac]
_ <8= _ [notation, in Vtac]
_ <7= _ [notation, in Vtac]
_ <6= _ [notation, in Vtac]
_ <5= _ [notation, in Vtac]
_ <4= _ [notation, in Vtac]
_ <3= _ [notation, in Vtac]
_ <2= _ [notation, in Vtac]
_ <1= _ [notation, in Vtac]
<< _ >> [notation, in Vtac]
<< _ : _ >> [notation, in Vtac]
Lemma Index
A
allowed_taskid_upd [in proofs]app_stack_app [in proofs]
app_stack1 [in proofs]
C
cexp_rel_right_mult [in proofs]cexp_rel_preserve [in proofs]
cexp_rel_right_det [in proofs]
cexp_rel_left_det [in proofs]
Completeness [in proofs]
completeness_one_step [in proofs]
completeness_ss [in proofs]
Correctness [in proofs]
count_empty [in proofs]
count_nonneg [in proofs]
count_list_deque [in proofs]
count_list_stack [in proofs]
count_list_app [in proofs]
count_update [in proofs]
count_rec_upd [in proofs]
count_split [in proofs]
count_helper [in proofs]
count1 [in proofs]
count1_int [in proofs]
count2 [in proofs]
D
deque_taskids_app [in proofs]E
eq_termvar [in lang]exp_app_app [in proofs]
F
fail_step [in proofs]ff_deterministic [in proofs]
finished_stable [in proofs]
fp_deterministic [in proofs]
fp_recover_transitivity [in proofs]
fp_implies_ff [in proofs]
G
geq_transitive [in proofs]geq_impl_pseq [in proofs]
geq_reflexive [in proofs]
I
indeq_step [in proofs]in_list_minus2 [in basis]
in_list_minus2I [in basis]
in_list_minus [in basis]
in_list_minusI [in basis]
in_map_fst [in basis]
In_right_deq [in proofs]
in_count [in proofs]
L
letFirst [in proofs]list_disj_minus2_mon [in basis]
list_disj_map_fst_minus2 [in basis]
list_assoc_flip [in basis]
list_disj_spec [in basis]
list_disj_mon_r [in basis]
list_disj_mon_l [in basis]
list_disj_minus_r [in basis]
list_disj_minus_l [in basis]
list_disj_app_l [in basis]
list_disj_app_r [in basis]
list_disj_app_rD [in basis]
list_disj_app_rI [in basis]
list_disj_comm [in basis]
list_disj_cons_l [in basis]
list_minus2_eq [in basis]
list_map_fst_minus2 [in basis]
list_minus2_remdup2 [in basis]
list_minus2_comm [in basis]
list_minus2_app_r [in basis]
list_minus2_app [in basis]
list_minus_swap [in basis]
list_minus_red [in basis]
list_minus_map_fst [in basis]
list_minus_comm [in basis]
list_minus_app_r [in basis]
list_minus_app [in basis]
list_assoc_someD [in basis]
list_assoc_noneD [in basis]
list_assoc_spec [in basis]
list_assoc_remdup2 [in basis]
list_assoc_minus2 [in basis]
list_assoc_app [in basis]
list_mem_map_fst [in basis]
list_mem_eq [in basis]
list_mem_spec [in basis]
list_mem_remdup [in basis]
list_mem_minus [in basis]
list_mem_app [in basis]
list_sum_nonneg [in proofs]
list_sum_app [in proofs]
M
map_snd_map_pair [in basis]map_fst_map_pair [in basis]
mp [in Vtac]
mpstep_completeness [in proofs]
mpstep_soundness [in proofs]
mpstep_right [in proofs]
mpstep_left [in proofs]
mpstep_neither [in proofs]
mpstep_star_trans [in proofs]
mpstep_star_one [in proofs]
N
nat_eq [in proofs]NoDup_app [in proofs]
nodup_count [in proofs]
P
pairFirst [in proofs]pairSecond [in proofs]
pm_istid_nonneg [in proofs]
Progress [in proofs]
R
recover_tuple [in lang]recover_implies_fp [in proofs]
reducef_tuple [in lang]
res_combine_results [in combine_results]
res_combine_rletr [in combine_results]
res_combine_rletl [in combine_results]
res_combine_bot [in combine_results]
res_combine_ptuple [in combine_results]
res_combine_values [in combine_results]
rm_istid_nonneg [in proofs]
rm_run [in proofs]
rm_ru [in proofs]
rm_ruo [in proofs]
rm_rus [in proofs]
run_step [in proofs]
S
soundness_ss [in proofs]soundness_helper_ss [in proofs]
ss_star_pair [in proofs]
ss_star_exp_app [in proofs]
ss_impl_mpstep_s_start [in proofs]
ss_impl_mpstep_s [in proofs]
ss_star_trans [in proofs]
ss_star_one [in proofs]
stack_decomp [in proofs]
stack_last_app [in proofs]
stack_app_det_right [in proofs]
stack_app_det_left [in proofs]
stack_taskids_app [in proofs]
stack_istid_nonneg [in proofs]
start_step [in proofs]
step_exp_app [in proofs]
step_app_stack [in proofs]
T
task_istid_nonneg [in proofs]V
vlib__andb_split [in Vtac]vlib__negb_rewrite [in Vtac]
vlib__not_false_is_true [in Vtac]
vlib__true_is_true [in Vtac]
W
wf_preserved [in proofs]wf_nd_altI [in proofs]
wf_prnd [in proofs]
wf_rrnd [in proofs]
wf_ppnd [in proofs]
wf_preserved_nd [in proofs]
Section Index
L
ListDefs [in basis]Notation Index
other
_ # _ [in combine_results]_ <12= _ [in Vtac]
_ <11= _ [in Vtac]
_ <10= _ [in Vtac]
_ <9= _ [in Vtac]
_ <8= _ [in Vtac]
_ <7= _ [in Vtac]
_ <6= _ [in Vtac]
_ <5= _ [in Vtac]
_ <4= _ [in Vtac]
_ <3= _ [in Vtac]
_ <2= _ [in Vtac]
_ <1= _ [in Vtac]
<< _ >> [in Vtac]
<< _ : _ >> [in Vtac]
Constructor Index
B
B_finished [in lang]B_right [in lang]
B_left [in lang]
B_neither [in lang]
C
cexp_rel_right_Right [in proofs]cexp_rel_right_Left [in proofs]
cexp_rel_right_Neither [in proofs]
cexp_rel_right_Finished [in proofs]
cexp_rel_right_Fail [in proofs]
cexp_rel_right_Run [in proofs]
cexp_rel_right_Start [in proofs]
cexp_rel_right_Thunk [in proofs]
cexp_rel_left_Right [in proofs]
cexp_rel_left_Left [in proofs]
cexp_rel_left_Neither [in proofs]
cexp_rel_left_Finished [in proofs]
cexp_rel_left_Fail [in proofs]
cexp_rel_left_Run [in proofs]
cexp_rel_left_Start [in proofs]
C_letL [in lang]
C_pairR [in lang]
C_pairL [in lang]
E
Eapp [in lang]Efst [in lang]
Eifnz [in lang]
Elet [in lang]
Epair [in lang]
Eplus [in lang]
Esnd [in lang]
Eval [in lang]
G
Geq_letr2 [in proofs]Geq_letr1 [in proofs]
Geq_letl [in proofs]
Geq_Ptuple [in proofs]
Geq_Val [in proofs]
Geq_Bot [in proofs]
M
mpstep_right_last [in lang]mpstep_right_first [in lang]
mpstep_left_last [in lang]
mpstep_left_first [in lang]
mpstep_pop_task [in lang]
mpstep_local [in lang]
mpstep_steal [in lang]
mpstep_recover [in lang]
mpstep_fork [in lang]
mpstep_starT [in proofs]
mpstep_starR [in proofs]
P
PCfail [in lang]PCfinish [in lang]
PCrecover [in lang]
PCrun [in lang]
PCstart [in lang]
PSeq_letr2 [in proofs]
PSeq_letl [in proofs]
PSeq_Ptuple [in proofs]
PSeq_Val [in proofs]
PSeq_Bot [in proofs]
R
Rbot [in lang]recover_ptuple [in lang]
recover_letRF [in lang]
recover_letRS [in lang]
recover_letLFR [in lang]
recover_letLFL [in lang]
recover_letLS [in lang]
recover_bottom [in lang]
recover_init [in lang]
recover_starT [in proofs]
recover_starR [in proofs]
reducef_letFR [in lang]
reducef_letFL [in lang]
reducef_bottom [in lang]
reducef_ptuple [in lang]
reducef_if_false [in lang]
reducef_if_true [in lang]
reducef_second [in lang]
reducef_first [in lang]
reducef_app [in lang]
reducef_let [in lang]
reducef_plus [in lang]
reducef_init [in lang]
reduce_ptuple [in lang]
reduce_if_false [in lang]
reduce_if_true [in lang]
reduce_second [in lang]
reduce_first [in lang]
reduce_app [in lang]
reduce_let [in lang]
reduce_plus [in lang]
reduce_init [in lang]
Rletl [in lang]
Rletr [in lang]
Rptuple [in lang]
Rval [in lang]
S
spstep_fail [in lang]spstep_apply_context [in lang]
spstep_push_context [in lang]
spstep_run [in lang]
spstep_eval [in lang]
ss_starT [in proofs]
ss_starR [in proofs]
step_par_join [in lang]
step_par_right [in lang]
step_par_left [in lang]
step_ifnz_false [in lang]
step_ifnz_true [in lang]
step_second [in lang]
step_first [in lang]
step_app [in lang]
step_letII [in lang]
step_letI [in lang]
step_plus [in lang]
S_cons [in lang]
S_right [in lang]
S_left [in lang]
T
TIDleft [in lang]TIDright [in lang]
T_right [in lang]
V
Vfunc [in lang]Vint [in lang]
Vpair [in lang]
Vvar [in lang]
Inductive Index
B
branch [in lang]C
cexp_rel_right [in proofs]cexp_rel_left [in proofs]
context [in lang]
E
exp [in lang]G
geq [in proofs]M
mpstep [in lang]mpstep_star [in proofs]
P
proc_config [in lang]pseq [in proofs]
R
recover [in lang]recover_star [in proofs]
reduce [in lang]
reducef [in lang]
res [in lang]
S
spstep [in lang]ss_star [in proofs]
stack [in lang]
step [in lang]
T
task [in lang]taskid [in lang]
V
val [in lang]Definition Index
A
allowed_taskid [in proofs]appctx_context_exp [in lang]
app_stack [in proofs]
C
cexp_rel_ind [in proofs]cexp_rel_right_ind1 [in proofs]
cexp_rel_left_ind1 [in proofs]
count [in proofs]
count_list [in proofs]
count_rec [in proofs]
D
deque [in lang]deque_taskids [in proofs]
E
empty_map [in lang]exp_not_value [in lang]
exp_app [in proofs]
F
ffun [in lang]ff_update [in lang]
I
identifier [in lang]is_zero [in lang]
is_true [in Vtac]
L
list_remdup2 [in basis]list_remdup [in basis]
list_disj [in basis]
list_minus2 [in basis]
list_minus [in basis]
list_assoc [in basis]
list_mem [in basis]
list_sum [in proofs]
M
map_pair [in basis]N
not_value [in lang]NW [in Vtac]
P
pidentifier [in lang]pm_istid [in proofs]
proc_map [in lang]
R
result_map [in lang]res_combine [in lang]
rm_istid [in proofs]
rm_taskids [in proofs]
S
stack_istid [in proofs]stack_taskids [in proofs]
stack_conts [in proofs]
stack_last [in proofs]
stack_app [in proofs]
subst_proc_config [in lang]
subst_branch [in lang]
subst_res [in lang]
subst_task [in lang]
subst_stack [in lang]
subst_context [in lang]
subst_exp [in lang]
subst_val [in lang]
T
taskids [in proofs]task_istid [in proofs]
termvar [in lang]
tid_eq [in proofs]
W
well_formed [in proofs]well_formed_nd_alt [in proofs]
well_formed_nd [in proofs]
Variable Index
L
ListDefs.A [in basis]ListDefs.B [in basis]
ListDefs.C [in basis]
ListDefs.D [in basis]
ListDefs.myeq [in basis]
Library Index
B
basisC
combine_resultsL
langP
proofsV
Vtac| 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 | (370 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 | (144 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 | (1 entry) |
| 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 | (15 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 | (121 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 | (22 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 | (57 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 | (5 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 | (5 entries) |
This page has been generated by coqdoc