| 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 | (397 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 | (1 entry) |
| 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 | (32 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 | (7 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 | (105 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 | (94 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 | (23 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 | (6 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 | (6 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 | (1 entry) |
| 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 | (122 entries) |
Global Index
A
abs_imp [library]abs_functional_metatheory [library]
abs_defs [library]
abs_examples [library]
abs_imperative_metatheory [library]
abs_util [library]
add [definition, in ABS.abs_imp]
addG_subG [lemma, in ABS.abs_util]
add_G [definition, in ABS.abs_util]
B
b [definition, in ABS.abs_defs]bind [definition, in ABS.abs_imp]
bind_params [definition, in ABS.abs_imp]
bind_params_aux [definition, in ABS.abs_imp]
bind_wt [lemma, in ABS.abs_imperative_metatheory]
C
C [definition, in ABS.abs_defs]CL [inductive, in ABS.abs_defs]
class [constructor, in ABS.abs_defs]
CL_sind [definition, in ABS.abs_defs]
CL_rec [definition, in ABS.abs_defs]
CL_ind [definition, in ABS.abs_defs]
CL_rect [definition, in ABS.abs_defs]
CL_wt_add_f [lemma, in ABS.abs_imperative_metatheory]
CL_wt_fields_fresh [lemma, in ABS.abs_imperative_metatheory]
CL_well_typed [definition, in ABS.abs_imperative_metatheory]
cn [inductive, in ABS.abs_defs]
cn_sind [definition, in ABS.abs_defs]
cn_rec [definition, in ABS.abs_defs]
cn_ind [definition, in ABS.abs_defs]
cn_rect [definition, in ABS.abs_defs]
cn_invoc [constructor, in ABS.abs_defs]
cn_object [constructor, in ABS.abs_defs]
cn_future [constructor, in ABS.abs_defs]
cn_well_typed [inductive, in ABS.abs_imperative_metatheory]
combine_map [lemma, in ABS.list_util]
combine_app [lemma, in ABS.list_util]
combine_snd [lemma, in ABS.list_util]
combine_nil [lemma, in ABS.list_util]
combine_fst [lemma, in ABS.list_util]
config [definition, in ABS.abs_imp]
config_well_typed [definition, in ABS.abs_imperative_metatheory]
cons_neq [lemma, in ABS.list_util]
countable_task [instance, in ABS.abs_defs]
Ctx [definition, in ABS.abs_examples]
ctxv [inductive, in ABS.abs_defs]
ctxv_sind [definition, in ABS.abs_defs]
ctxv_rec [definition, in ABS.abs_defs]
ctxv_ind [definition, in ABS.abs_defs]
ctxv_rect [definition, in ABS.abs_defs]
ctxv_fut [constructor, in ABS.abs_defs]
ctxv_sig [constructor, in ABS.abs_defs]
ctxv_T [constructor, in ABS.abs_defs]
D
destiny [definition, in ABS.abs_imp]disjoint_monotone [lemma, in ABS.abs_util]
E
e [inductive, in ABS.abs_defs]eq_z [lemma, in ABS.abs_defs]
eq_C [lemma, in ABS.abs_defs]
eq_m [lemma, in ABS.abs_defs]
eq_o [lemma, in ABS.abs_defs]
eq_f [lemma, in ABS.abs_defs]
eq_fut [lemma, in ABS.abs_defs]
eq_x [lemma, in ABS.abs_defs]
eq_fc [lemma, in ABS.abs_defs]
eq_i [lemma, in ABS.abs_defs]
eval [definition, in ABS.abs_imp]
eval_list [definition, in ABS.abs_imp]
extend_subG_2 [lemma, in ABS.abs_util]
extend_domain [lemma, in ABS.abs_util]
extend_subG [lemma, in ABS.abs_util]
extend_G [definition, in ABS.abs_util]
e_call_const_5_T_int [lemma, in ABS.abs_examples]
e_call_const_typ_F [lemma, in ABS.abs_examples]
e_const_5_T_int [lemma, in ABS.abs_examples]
e_call_const_5 [definition, in ABS.abs_examples]
e_const_5 [definition, in ABS.abs_examples]
e_subst_list_s [definition, in ABS.abs_util]
e_subst_s [definition, in ABS.abs_util]
e_list_fresh [lemma, in ABS.abs_util]
e_list_subst [lemma, in ABS.abs_util]
e_list_subst_map [lemma, in ABS.abs_util]
e_eq_dec [instance, in ABS.abs_defs]
e_ott_rec [definition, in ABS.abs_defs]
e_rec.H_list_e_cons [variable, in ABS.abs_defs]
e_rec.H_list_e_nil [variable, in ABS.abs_defs]
e_rec.H_e_fn_call [variable, in ABS.abs_defs]
e_rec.H_e_lt [variable, in ABS.abs_defs]
e_rec.H_e_eq [variable, in ABS.abs_defs]
e_rec.H_e_mul [variable, in ABS.abs_defs]
e_rec.H_e_add [variable, in ABS.abs_defs]
e_rec.H_e_not [variable, in ABS.abs_defs]
e_rec.H_e_neg [variable, in ABS.abs_defs]
e_rec.H_e_var [variable, in ABS.abs_defs]
e_rec.H_e_t [variable, in ABS.abs_defs]
e_rec.P_list_e [variable, in ABS.abs_defs]
e_rec.P_e [variable, in ABS.abs_defs]
e_rec [section, in ABS.abs_defs]
e_var_subst [definition, in ABS.abs_defs]
e_list_subst_one [definition, in ABS.abs_defs]
e_var_subst_one [definition, in ABS.abs_defs]
e_ott_ind [definition, in ABS.abs_defs]
e_rect.H_list_e_cons [variable, in ABS.abs_defs]
e_rect.H_list_e_nil [variable, in ABS.abs_defs]
e_rect.H_e_lt [variable, in ABS.abs_defs]
e_rect.H_e_eq [variable, in ABS.abs_defs]
e_rect.H_e_mul [variable, in ABS.abs_defs]
e_rect.H_e_add [variable, in ABS.abs_defs]
e_rect.H_e_not [variable, in ABS.abs_defs]
e_rect.H_e_neg [variable, in ABS.abs_defs]
e_rect.H_e_fn_call [variable, in ABS.abs_defs]
e_rect.H_e_var [variable, in ABS.abs_defs]
e_rect.H_e_t [variable, in ABS.abs_defs]
e_rect.P_e [variable, in ABS.abs_defs]
e_rect.P_list_e [variable, in ABS.abs_defs]
e_rect [section, in ABS.abs_defs]
e_sind [definition, in ABS.abs_defs]
e_rec [definition, in ABS.abs_defs]
e_ind [definition, in ABS.abs_defs]
e_rect [definition, in ABS.abs_defs]
e_lt [constructor, in ABS.abs_defs]
e_eq [constructor, in ABS.abs_defs]
e_mul [constructor, in ABS.abs_defs]
e_add [constructor, in ABS.abs_defs]
e_not [constructor, in ABS.abs_defs]
e_neg [constructor, in ABS.abs_defs]
e_fn_call [constructor, in ABS.abs_defs]
e_var [constructor, in ABS.abs_defs]
e_t [constructor, in ABS.abs_defs]
F
F [inductive, in ABS.abs_defs]f [definition, in ABS.abs_defs]
fc [definition, in ABS.abs_defs]
fold_map5 [lemma, in ABS.abs_functional_metatheory]
fold_map4 [lemma, in ABS.abs_functional_metatheory]
fold_add_comm [lemma, in ABS.abs_util]
fold_map_reshuffle [lemma, in ABS.abs_util]
fold_map5 [lemma, in ABS.list_util]
fold_map4 [lemma, in ABS.list_util]
fold_map3 [lemma, in ABS.list_util]
fold_map2 [lemma, in ABS.list_util]
fold_map1 [lemma, in ABS.list_util]
fold_map [lemma, in ABS.list_util]
Forall_typ_F_extension [lemma, in ABS.abs_imperative_metatheory]
fresh [definition, in ABS.abs_imp]
fresh_consistent [lemma, in ABS.abs_functional_metatheory]
fresh_subG [lemma, in ABS.abs_functional_metatheory]
fresh_var_subst [lemma, in ABS.abs_util]
fresh_monotone_el [lemma, in ABS.abs_util]
fresh_first_el [lemma, in ABS.abs_util]
fresh_monotone_e [lemma, in ABS.abs_util]
fresh_first_e [lemma, in ABS.abs_util]
fresh_vars [definition, in ABS.abs_defs]
fresh_vars_s [definition, in ABS.abs_defs]
fresh_vars_el [definition, in ABS.abs_defs]
fresh_vars_e [definition, in ABS.abs_defs]
fresh_extend_wt [lemma, in ABS.abs_imperative_metatheory]
fresh_config_wt [lemma, in ABS.abs_imperative_metatheory]
FunctionalMetatheory [section, in ABS.abs_functional_metatheory]
FunctionalMetatheory.vars_fs_distinct [variable, in ABS.abs_functional_metatheory]
_ G⊢ _ [notation, in ABS.abs_functional_metatheory]
func_const_5 [definition, in ABS.abs_examples]
fut [definition, in ABS.abs_defs]
fut_wt_some [constructor, in ABS.abs_imperative_metatheory]
fut_wt_none [constructor, in ABS.abs_imperative_metatheory]
F_sind [definition, in ABS.abs_defs]
F_rec [definition, in ABS.abs_defs]
F_ind [definition, in ABS.abs_defs]
F_rect [definition, in ABS.abs_defs]
F_fn [constructor, in ABS.abs_defs]
G
G [definition, in ABS.abs_defs]get_type [definition, in ABS.abs_functional_metatheory]
get_class_decl_some [lemma, in ABS.abs_imp]
get_class_decl [definition, in ABS.abs_imp]
get_method_decl [definition, in ABS.abs_imp]
get_type [definition, in ABS.abs_imp]
get_params [definition, in ABS.abs_imp]
get_methods [definition, in ABS.abs_imp]
get_fields [definition, in ABS.abs_imp]
get_class_name [definition, in ABS.abs_imp]
G_vdash_s [definition, in ABS.abs_functional_metatheory]
G_vdash_union [lemma, in ABS.abs_imperative_metatheory]
I
i [definition, in ABS.abs_defs]id [abbreviation, in ABS.abs_imp]
insert_lookup_ne_extend [lemma, in ABS.abs_imperative_metatheory]
inv_wt [constructor, in ABS.abs_imperative_metatheory]
in_fst_iff [lemma, in ABS.list_util]
in_combine_split [lemma, in ABS.list_util]
in_split [lemma, in ABS.list_util]
in_combine [lemma, in ABS.list_util]
is_fut_intro [constructor, in ABS.abs_imp]
is_fut [inductive, in ABS.abs_imp]
L
ListLemmas [section, in ABS.list_util]list_util [library]
local_well_typed [definition, in ABS.abs_functional_metatheory]
M
M [inductive, in ABS.abs_defs]m [definition, in ABS.abs_defs]
MapLemmas [section, in ABS.abs_util]
map_neq_none_is_some [lemma, in ABS.abs_util]
map_split' [lemma, in ABS.list_util]
map_xs [lemma, in ABS.list_util]
map_split [lemma, in ABS.list_util]
map_eq [lemma, in ABS.list_util]
match_intro [constructor, in ABS.abs_imperative_metatheory]
match_method [inductive, in ABS.abs_imperative_metatheory]
M_sind [definition, in ABS.abs_defs]
M_rec [definition, in ABS.abs_defs]
M_ind [definition, in ABS.abs_defs]
M_rect [definition, in ABS.abs_defs]
M_m [constructor, in ABS.abs_defs]
N
neq_none_is_some [lemma, in ABS.abs_util]O
o [definition, in ABS.abs_defs]ob_wt [constructor, in ABS.abs_imperative_metatheory]
P
P [inductive, in ABS.abs_defs]pat2_id [lemma, in ABS.list_util]
program [constructor, in ABS.abs_defs]
P_sind [definition, in ABS.abs_defs]
P_rec [definition, in ABS.abs_defs]
P_ind [definition, in ABS.abs_defs]
P_rect [definition, in ABS.abs_defs]
Q
queue [definition, in ABS.abs_defs]queue_well_typed [definition, in ABS.abs_imperative_metatheory]
q_wt_add [lemma, in ABS.abs_imperative_metatheory]
q_wt_remove [lemma, in ABS.abs_imperative_metatheory]
R
reduce [definition, in ABS.abs_functional_metatheory]red_e_sind [definition, in ABS.abs_defs]
red_e_ind [definition, in ABS.abs_defs]
red_fun_ground [constructor, in ABS.abs_defs]
red_fun_exp [constructor, in ABS.abs_defs]
red_lt_r [constructor, in ABS.abs_defs]
red_lt_l [constructor, in ABS.abs_defs]
red_eq_r [constructor, in ABS.abs_defs]
red_eq_l [constructor, in ABS.abs_defs]
red_mul_r [constructor, in ABS.abs_defs]
red_mul_l [constructor, in ABS.abs_defs]
red_add_r [constructor, in ABS.abs_defs]
red_add_l [constructor, in ABS.abs_defs]
red_not' [constructor, in ABS.abs_defs]
red_neg' [constructor, in ABS.abs_defs]
red_lt [constructor, in ABS.abs_defs]
red_eq [constructor, in ABS.abs_defs]
red_mul [constructor, in ABS.abs_defs]
red_add [constructor, in ABS.abs_defs]
red_not [constructor, in ABS.abs_defs]
red_neg [constructor, in ABS.abs_defs]
red_var [constructor, in ABS.abs_defs]
red_e [inductive, in ABS.abs_defs]
remove [definition, in ABS.abs_imp]
replace_var [definition, in ABS.abs_util]
rhs [inductive, in ABS.abs_defs]
rhs_eq_dec [instance, in ABS.abs_defs]
rhs_sind [definition, in ABS.abs_defs]
rhs_rec [definition, in ABS.abs_defs]
rhs_ind [definition, in ABS.abs_defs]
rhs_rect [definition, in ABS.abs_defs]
rhs_get [constructor, in ABS.abs_defs]
rhs_invoc [constructor, in ABS.abs_defs]
rhs_e [constructor, in ABS.abs_defs]
S
s [definition, in ABS.abs_defs]same_type_sub [lemma, in ABS.abs_functional_metatheory]
sig [inductive, in ABS.abs_defs]
sig_sind [definition, in ABS.abs_defs]
sig_rec [definition, in ABS.abs_defs]
sig_ind [definition, in ABS.abs_defs]
sig_rect [definition, in ABS.abs_defs]
sig_sig [constructor, in ABS.abs_defs]
split_corresponding_list_no_length [lemma, in ABS.list_util]
split_corresponding_list [lemma, in ABS.list_util]
step_load [constructor, in ABS.abs_imp]
step_read [constructor, in ABS.abs_imp]
step_return [constructor, in ABS.abs_imp]
step_call [constructor, in ABS.abs_imp]
step_while [constructor, in ABS.abs_imp]
step_skip2 [constructor, in ABS.abs_imp]
step_skip1 [constructor, in ABS.abs_imp]
step_cond2 [constructor, in ABS.abs_imp]
step_cond1 [constructor, in ABS.abs_imp]
step_asgn2 [constructor, in ABS.abs_imp]
step_asgn1 [constructor, in ABS.abs_imp]
step_activate [constructor, in ABS.abs_imp]
stmt [inductive, in ABS.abs_defs]
stmt_step_sind [definition, in ABS.abs_imp]
stmt_step_ind [definition, in ABS.abs_imp]
stmt_step [inductive, in ABS.abs_imp]
stmt_eq_dec [instance, in ABS.abs_defs]
stmt_sind [definition, in ABS.abs_defs]
stmt_rec [definition, in ABS.abs_defs]
stmt_ind [definition, in ABS.abs_defs]
stmt_rect [definition, in ABS.abs_defs]
stmt_ret [constructor, in ABS.abs_defs]
stmt_loop [constructor, in ABS.abs_defs]
stmt_cond [constructor, in ABS.abs_defs]
stmt_asgn [constructor, in ABS.abs_defs]
stmt_skip [constructor, in ABS.abs_defs]
stmt_seq [constructor, in ABS.abs_defs]
stmt_well_typed_sind [definition, in ABS.abs_imperative_metatheory]
stmt_well_typed_ind [definition, in ABS.abs_imperative_metatheory]
stmt_well_typed_return [constructor, in ABS.abs_imperative_metatheory]
stmt_well_typed_loop [constructor, in ABS.abs_imperative_metatheory]
stmt_well_typed_cond [constructor, in ABS.abs_imperative_metatheory]
stmt_well_typed_asgn [constructor, in ABS.abs_imperative_metatheory]
stmt_well_typed_skip [constructor, in ABS.abs_imperative_metatheory]
stmt_well_typed [inductive, in ABS.abs_imperative_metatheory]
subG_typ_F_forall [lemma, in ABS.abs_functional_metatheory]
subG_typ_F [lemma, in ABS.abs_functional_metatheory]
subG_foldr [lemma, in ABS.abs_functional_metatheory]
subG_type [lemma, in ABS.abs_functional_metatheory]
subG_consistent [lemma, in ABS.abs_functional_metatheory]
subG_extend [lemma, in ABS.abs_util]
subG_add_2 [lemma, in ABS.abs_util]
subG_add [lemma, in ABS.abs_util]
subG_sub_wt [lemma, in ABS.abs_util]
subG_queue_wt [lemma, in ABS.abs_imperative_metatheory]
subG_task_wt [lemma, in ABS.abs_imperative_metatheory]
subG_stmt_wt [lemma, in ABS.abs_imperative_metatheory]
subG_typ_rhs [lemma, in ABS.abs_imperative_metatheory]
subG_typ_es [lemma, in ABS.abs_imperative_metatheory]
subst_lemma [lemma, in ABS.abs_functional_metatheory]
subst_lemma_one [lemma, in ABS.abs_functional_metatheory]
subst_lt [lemma, in ABS.abs_util]
subst_eq [lemma, in ABS.abs_util]
subst_mul [lemma, in ABS.abs_util]
subst_add [lemma, in ABS.abs_util]
subst_not [lemma, in ABS.abs_util]
subst_neg [lemma, in ABS.abs_util]
subst_fn [lemma, in ABS.abs_util]
subst_var [lemma, in ABS.abs_util]
subst_term [lemma, in ABS.abs_util]
subst_snd_commutes [lemma, in ABS.abs_util]
subst_fst_commute [lemma, in ABS.abs_util]
sub_well_typed [definition, in ABS.abs_util]
T
T [inductive, in ABS.abs_defs]t [inductive, in ABS.abs_defs]
task [inductive, in ABS.abs_defs]
tasko [definition, in ABS.abs_defs]
task_eq_dec [instance, in ABS.abs_defs]
task_sind [definition, in ABS.abs_defs]
task_rec [definition, in ABS.abs_defs]
task_ind [definition, in ABS.abs_defs]
task_rect [definition, in ABS.abs_defs]
task_wt [constructor, in ABS.abs_imperative_metatheory]
task_wt_idle [constructor, in ABS.abs_imperative_metatheory]
task_well_typed [inductive, in ABS.abs_imperative_metatheory]
to [definition, in ABS.abs_defs]
tsk [constructor, in ABS.abs_defs]
type_preservation [lemma, in ABS.abs_functional_metatheory]
type_preservation_step [lemma, in ABS.abs_functional_metatheory]
type_preservation [lemma, in ABS.abs_imperative_metatheory]
type_preservation_eval_list [lemma, in ABS.abs_imperative_metatheory]
type_preservation_eval [lemma, in ABS.abs_imperative_metatheory]
Typing [section, in ABS.abs_imperative_metatheory]
Typing.id_of_name_of [variable, in ABS.abs_imperative_metatheory]
Typing.id_of_well_typed [variable, in ABS.abs_imperative_metatheory]
Typing.id_of_consistent [variable, in ABS.abs_imperative_metatheory]
Typing.name_of_id_of [variable, in ABS.abs_imperative_metatheory]
Typing.vars_fs_distinct [variable, in ABS.abs_imperative_metatheory]
typ_e_G_Equal_equiv [lemma, in ABS.abs_functional_metatheory]
typ_e_G_Equal_equiv_imp [lemma, in ABS.abs_functional_metatheory]
typ_es [definition, in ABS.abs_util]
typ_F_sind [definition, in ABS.abs_defs]
typ_F_ind [definition, in ABS.abs_defs]
typ_func_decl [constructor, in ABS.abs_defs]
typ_F [inductive, in ABS.abs_defs]
typ_e_sind [definition, in ABS.abs_defs]
typ_e_ind [definition, in ABS.abs_defs]
typ_func_expr [constructor, in ABS.abs_defs]
typ_lt [constructor, in ABS.abs_defs]
typ_eq [constructor, in ABS.abs_defs]
typ_mul [constructor, in ABS.abs_defs]
typ_add [constructor, in ABS.abs_defs]
typ_not [constructor, in ABS.abs_defs]
typ_neg [constructor, in ABS.abs_defs]
typ_var [constructor, in ABS.abs_defs]
typ_int [constructor, in ABS.abs_defs]
typ_bool [constructor, in ABS.abs_defs]
typ_e [inductive, in ABS.abs_defs]
typ_stmt_seq [constructor, in ABS.abs_imperative_metatheory]
typ_rhs_get [constructor, in ABS.abs_imperative_metatheory]
typ_rhs_invoc [constructor, in ABS.abs_imperative_metatheory]
typ_rhs_e [constructor, in ABS.abs_imperative_metatheory]
typ_rhs [inductive, in ABS.abs_imperative_metatheory]
typ_term_list_invariant [lemma, in ABS.abs_imperative_metatheory]
typ_term_invariant [lemma, in ABS.abs_imperative_metatheory]
t_eq_dec [instance, in ABS.abs_defs]
T_sind [definition, in ABS.abs_defs]
T_rec [definition, in ABS.abs_defs]
T_ind [definition, in ABS.abs_defs]
T_rect [definition, in ABS.abs_defs]
T_int [constructor, in ABS.abs_defs]
T_bool [constructor, in ABS.abs_defs]
t_sind [definition, in ABS.abs_defs]
t_rec [definition, in ABS.abs_defs]
t_ind [definition, in ABS.abs_defs]
t_rect [definition, in ABS.abs_defs]
t_fut [constructor, in ABS.abs_defs]
t_int [constructor, in ABS.abs_defs]
t_b [constructor, in ABS.abs_defs]
V
vdash_implies_wt [lemma, in ABS.abs_imperative_metatheory]W
well_formed [definition, in ABS.abs_defs]X
x [definition, in ABS.abs_defs]Z
z [definition, in ABS.abs_defs]Notation Index
F
_ G⊢ _ [in ABS.abs_functional_metatheory]Variable Index
E
e_rec.H_list_e_cons [in ABS.abs_defs]e_rec.H_list_e_nil [in ABS.abs_defs]
e_rec.H_e_fn_call [in ABS.abs_defs]
e_rec.H_e_lt [in ABS.abs_defs]
e_rec.H_e_eq [in ABS.abs_defs]
e_rec.H_e_mul [in ABS.abs_defs]
e_rec.H_e_add [in ABS.abs_defs]
e_rec.H_e_not [in ABS.abs_defs]
e_rec.H_e_neg [in ABS.abs_defs]
e_rec.H_e_var [in ABS.abs_defs]
e_rec.H_e_t [in ABS.abs_defs]
e_rec.P_list_e [in ABS.abs_defs]
e_rec.P_e [in ABS.abs_defs]
e_rect.H_list_e_cons [in ABS.abs_defs]
e_rect.H_list_e_nil [in ABS.abs_defs]
e_rect.H_e_lt [in ABS.abs_defs]
e_rect.H_e_eq [in ABS.abs_defs]
e_rect.H_e_mul [in ABS.abs_defs]
e_rect.H_e_add [in ABS.abs_defs]
e_rect.H_e_not [in ABS.abs_defs]
e_rect.H_e_neg [in ABS.abs_defs]
e_rect.H_e_fn_call [in ABS.abs_defs]
e_rect.H_e_var [in ABS.abs_defs]
e_rect.H_e_t [in ABS.abs_defs]
e_rect.P_e [in ABS.abs_defs]
e_rect.P_list_e [in ABS.abs_defs]
F
FunctionalMetatheory.vars_fs_distinct [in ABS.abs_functional_metatheory]T
Typing.id_of_name_of [in ABS.abs_imperative_metatheory]Typing.id_of_well_typed [in ABS.abs_imperative_metatheory]
Typing.id_of_consistent [in ABS.abs_imperative_metatheory]
Typing.name_of_id_of [in ABS.abs_imperative_metatheory]
Typing.vars_fs_distinct [in ABS.abs_imperative_metatheory]
Library Index
A
abs_impabs_functional_metatheory
abs_defs
abs_examples
abs_imperative_metatheory
abs_util
L
list_utilLemma Index
A
addG_subG [in ABS.abs_util]B
bind_wt [in ABS.abs_imperative_metatheory]C
CL_wt_add_f [in ABS.abs_imperative_metatheory]CL_wt_fields_fresh [in ABS.abs_imperative_metatheory]
combine_map [in ABS.list_util]
combine_app [in ABS.list_util]
combine_snd [in ABS.list_util]
combine_nil [in ABS.list_util]
combine_fst [in ABS.list_util]
cons_neq [in ABS.list_util]
D
disjoint_monotone [in ABS.abs_util]E
eq_z [in ABS.abs_defs]eq_C [in ABS.abs_defs]
eq_m [in ABS.abs_defs]
eq_o [in ABS.abs_defs]
eq_f [in ABS.abs_defs]
eq_fut [in ABS.abs_defs]
eq_x [in ABS.abs_defs]
eq_fc [in ABS.abs_defs]
eq_i [in ABS.abs_defs]
extend_subG_2 [in ABS.abs_util]
extend_domain [in ABS.abs_util]
extend_subG [in ABS.abs_util]
e_call_const_5_T_int [in ABS.abs_examples]
e_call_const_typ_F [in ABS.abs_examples]
e_const_5_T_int [in ABS.abs_examples]
e_list_fresh [in ABS.abs_util]
e_list_subst [in ABS.abs_util]
e_list_subst_map [in ABS.abs_util]
F
fold_map5 [in ABS.abs_functional_metatheory]fold_map4 [in ABS.abs_functional_metatheory]
fold_add_comm [in ABS.abs_util]
fold_map_reshuffle [in ABS.abs_util]
fold_map5 [in ABS.list_util]
fold_map4 [in ABS.list_util]
fold_map3 [in ABS.list_util]
fold_map2 [in ABS.list_util]
fold_map1 [in ABS.list_util]
fold_map [in ABS.list_util]
Forall_typ_F_extension [in ABS.abs_imperative_metatheory]
fresh_consistent [in ABS.abs_functional_metatheory]
fresh_subG [in ABS.abs_functional_metatheory]
fresh_var_subst [in ABS.abs_util]
fresh_monotone_el [in ABS.abs_util]
fresh_first_el [in ABS.abs_util]
fresh_monotone_e [in ABS.abs_util]
fresh_first_e [in ABS.abs_util]
fresh_extend_wt [in ABS.abs_imperative_metatheory]
fresh_config_wt [in ABS.abs_imperative_metatheory]
G
get_class_decl_some [in ABS.abs_imp]G_vdash_union [in ABS.abs_imperative_metatheory]
I
insert_lookup_ne_extend [in ABS.abs_imperative_metatheory]in_fst_iff [in ABS.list_util]
in_combine_split [in ABS.list_util]
in_split [in ABS.list_util]
in_combine [in ABS.list_util]
M
map_neq_none_is_some [in ABS.abs_util]map_split' [in ABS.list_util]
map_xs [in ABS.list_util]
map_split [in ABS.list_util]
map_eq [in ABS.list_util]
N
neq_none_is_some [in ABS.abs_util]P
pat2_id [in ABS.list_util]Q
q_wt_add [in ABS.abs_imperative_metatheory]q_wt_remove [in ABS.abs_imperative_metatheory]
S
same_type_sub [in ABS.abs_functional_metatheory]split_corresponding_list_no_length [in ABS.list_util]
split_corresponding_list [in ABS.list_util]
subG_typ_F_forall [in ABS.abs_functional_metatheory]
subG_typ_F [in ABS.abs_functional_metatheory]
subG_foldr [in ABS.abs_functional_metatheory]
subG_type [in ABS.abs_functional_metatheory]
subG_consistent [in ABS.abs_functional_metatheory]
subG_extend [in ABS.abs_util]
subG_add_2 [in ABS.abs_util]
subG_add [in ABS.abs_util]
subG_sub_wt [in ABS.abs_util]
subG_queue_wt [in ABS.abs_imperative_metatheory]
subG_task_wt [in ABS.abs_imperative_metatheory]
subG_stmt_wt [in ABS.abs_imperative_metatheory]
subG_typ_rhs [in ABS.abs_imperative_metatheory]
subG_typ_es [in ABS.abs_imperative_metatheory]
subst_lemma [in ABS.abs_functional_metatheory]
subst_lemma_one [in ABS.abs_functional_metatheory]
subst_lt [in ABS.abs_util]
subst_eq [in ABS.abs_util]
subst_mul [in ABS.abs_util]
subst_add [in ABS.abs_util]
subst_not [in ABS.abs_util]
subst_neg [in ABS.abs_util]
subst_fn [in ABS.abs_util]
subst_var [in ABS.abs_util]
subst_term [in ABS.abs_util]
subst_snd_commutes [in ABS.abs_util]
subst_fst_commute [in ABS.abs_util]
T
type_preservation [in ABS.abs_functional_metatheory]type_preservation_step [in ABS.abs_functional_metatheory]
type_preservation [in ABS.abs_imperative_metatheory]
type_preservation_eval_list [in ABS.abs_imperative_metatheory]
type_preservation_eval [in ABS.abs_imperative_metatheory]
typ_e_G_Equal_equiv [in ABS.abs_functional_metatheory]
typ_e_G_Equal_equiv_imp [in ABS.abs_functional_metatheory]
typ_term_list_invariant [in ABS.abs_imperative_metatheory]
typ_term_invariant [in ABS.abs_imperative_metatheory]
V
vdash_implies_wt [in ABS.abs_imperative_metatheory]Constructor Index
C
class [in ABS.abs_defs]cn_invoc [in ABS.abs_defs]
cn_object [in ABS.abs_defs]
cn_future [in ABS.abs_defs]
ctxv_fut [in ABS.abs_defs]
ctxv_sig [in ABS.abs_defs]
ctxv_T [in ABS.abs_defs]
E
e_lt [in ABS.abs_defs]e_eq [in ABS.abs_defs]
e_mul [in ABS.abs_defs]
e_add [in ABS.abs_defs]
e_not [in ABS.abs_defs]
e_neg [in ABS.abs_defs]
e_fn_call [in ABS.abs_defs]
e_var [in ABS.abs_defs]
e_t [in ABS.abs_defs]
F
fut_wt_some [in ABS.abs_imperative_metatheory]fut_wt_none [in ABS.abs_imperative_metatheory]
F_fn [in ABS.abs_defs]
I
inv_wt [in ABS.abs_imperative_metatheory]is_fut_intro [in ABS.abs_imp]
M
match_intro [in ABS.abs_imperative_metatheory]M_m [in ABS.abs_defs]
O
ob_wt [in ABS.abs_imperative_metatheory]P
program [in ABS.abs_defs]R
red_fun_ground [in ABS.abs_defs]red_fun_exp [in ABS.abs_defs]
red_lt_r [in ABS.abs_defs]
red_lt_l [in ABS.abs_defs]
red_eq_r [in ABS.abs_defs]
red_eq_l [in ABS.abs_defs]
red_mul_r [in ABS.abs_defs]
red_mul_l [in ABS.abs_defs]
red_add_r [in ABS.abs_defs]
red_add_l [in ABS.abs_defs]
red_not' [in ABS.abs_defs]
red_neg' [in ABS.abs_defs]
red_lt [in ABS.abs_defs]
red_eq [in ABS.abs_defs]
red_mul [in ABS.abs_defs]
red_add [in ABS.abs_defs]
red_not [in ABS.abs_defs]
red_neg [in ABS.abs_defs]
red_var [in ABS.abs_defs]
rhs_get [in ABS.abs_defs]
rhs_invoc [in ABS.abs_defs]
rhs_e [in ABS.abs_defs]
S
sig_sig [in ABS.abs_defs]step_load [in ABS.abs_imp]
step_read [in ABS.abs_imp]
step_return [in ABS.abs_imp]
step_call [in ABS.abs_imp]
step_while [in ABS.abs_imp]
step_skip2 [in ABS.abs_imp]
step_skip1 [in ABS.abs_imp]
step_cond2 [in ABS.abs_imp]
step_cond1 [in ABS.abs_imp]
step_asgn2 [in ABS.abs_imp]
step_asgn1 [in ABS.abs_imp]
step_activate [in ABS.abs_imp]
stmt_ret [in ABS.abs_defs]
stmt_loop [in ABS.abs_defs]
stmt_cond [in ABS.abs_defs]
stmt_asgn [in ABS.abs_defs]
stmt_skip [in ABS.abs_defs]
stmt_seq [in ABS.abs_defs]
stmt_well_typed_return [in ABS.abs_imperative_metatheory]
stmt_well_typed_loop [in ABS.abs_imperative_metatheory]
stmt_well_typed_cond [in ABS.abs_imperative_metatheory]
stmt_well_typed_asgn [in ABS.abs_imperative_metatheory]
stmt_well_typed_skip [in ABS.abs_imperative_metatheory]
T
task_wt [in ABS.abs_imperative_metatheory]task_wt_idle [in ABS.abs_imperative_metatheory]
tsk [in ABS.abs_defs]
typ_func_decl [in ABS.abs_defs]
typ_func_expr [in ABS.abs_defs]
typ_lt [in ABS.abs_defs]
typ_eq [in ABS.abs_defs]
typ_mul [in ABS.abs_defs]
typ_add [in ABS.abs_defs]
typ_not [in ABS.abs_defs]
typ_neg [in ABS.abs_defs]
typ_var [in ABS.abs_defs]
typ_int [in ABS.abs_defs]
typ_bool [in ABS.abs_defs]
typ_stmt_seq [in ABS.abs_imperative_metatheory]
typ_rhs_get [in ABS.abs_imperative_metatheory]
typ_rhs_invoc [in ABS.abs_imperative_metatheory]
typ_rhs_e [in ABS.abs_imperative_metatheory]
T_int [in ABS.abs_defs]
T_bool [in ABS.abs_defs]
t_fut [in ABS.abs_defs]
t_int [in ABS.abs_defs]
t_b [in ABS.abs_defs]
Inductive Index
C
CL [in ABS.abs_defs]cn [in ABS.abs_defs]
cn_well_typed [in ABS.abs_imperative_metatheory]
ctxv [in ABS.abs_defs]
E
e [in ABS.abs_defs]F
F [in ABS.abs_defs]I
is_fut [in ABS.abs_imp]M
M [in ABS.abs_defs]match_method [in ABS.abs_imperative_metatheory]
P
P [in ABS.abs_defs]R
red_e [in ABS.abs_defs]rhs [in ABS.abs_defs]
S
sig [in ABS.abs_defs]stmt [in ABS.abs_defs]
stmt_step [in ABS.abs_imp]
stmt_well_typed [in ABS.abs_imperative_metatheory]
T
T [in ABS.abs_defs]t [in ABS.abs_defs]
task [in ABS.abs_defs]
task_well_typed [in ABS.abs_imperative_metatheory]
typ_F [in ABS.abs_defs]
typ_e [in ABS.abs_defs]
typ_rhs [in ABS.abs_imperative_metatheory]
Section Index
E
e_rec [in ABS.abs_defs]e_rect [in ABS.abs_defs]
F
FunctionalMetatheory [in ABS.abs_functional_metatheory]L
ListLemmas [in ABS.list_util]M
MapLemmas [in ABS.abs_util]T
Typing [in ABS.abs_imperative_metatheory]Instance Index
C
countable_task [in ABS.abs_defs]E
e_eq_dec [in ABS.abs_defs]R
rhs_eq_dec [in ABS.abs_defs]S
stmt_eq_dec [in ABS.abs_defs]T
task_eq_dec [in ABS.abs_defs]t_eq_dec [in ABS.abs_defs]
Abbreviation Index
I
id [in ABS.abs_imp]Definition Index
A
add [in ABS.abs_imp]add_G [in ABS.abs_util]
B
b [in ABS.abs_defs]bind [in ABS.abs_imp]
bind_params [in ABS.abs_imp]
bind_params_aux [in ABS.abs_imp]
C
C [in ABS.abs_defs]CL_sind [in ABS.abs_defs]
CL_rec [in ABS.abs_defs]
CL_ind [in ABS.abs_defs]
CL_rect [in ABS.abs_defs]
CL_well_typed [in ABS.abs_imperative_metatheory]
cn_sind [in ABS.abs_defs]
cn_rec [in ABS.abs_defs]
cn_ind [in ABS.abs_defs]
cn_rect [in ABS.abs_defs]
config [in ABS.abs_imp]
config_well_typed [in ABS.abs_imperative_metatheory]
Ctx [in ABS.abs_examples]
ctxv_sind [in ABS.abs_defs]
ctxv_rec [in ABS.abs_defs]
ctxv_ind [in ABS.abs_defs]
ctxv_rect [in ABS.abs_defs]
D
destiny [in ABS.abs_imp]E
eval [in ABS.abs_imp]eval_list [in ABS.abs_imp]
extend_G [in ABS.abs_util]
e_call_const_5 [in ABS.abs_examples]
e_const_5 [in ABS.abs_examples]
e_subst_list_s [in ABS.abs_util]
e_subst_s [in ABS.abs_util]
e_ott_rec [in ABS.abs_defs]
e_var_subst [in ABS.abs_defs]
e_list_subst_one [in ABS.abs_defs]
e_var_subst_one [in ABS.abs_defs]
e_ott_ind [in ABS.abs_defs]
e_sind [in ABS.abs_defs]
e_rec [in ABS.abs_defs]
e_ind [in ABS.abs_defs]
e_rect [in ABS.abs_defs]
F
f [in ABS.abs_defs]fc [in ABS.abs_defs]
fresh [in ABS.abs_imp]
fresh_vars [in ABS.abs_defs]
fresh_vars_s [in ABS.abs_defs]
fresh_vars_el [in ABS.abs_defs]
fresh_vars_e [in ABS.abs_defs]
func_const_5 [in ABS.abs_examples]
fut [in ABS.abs_defs]
F_sind [in ABS.abs_defs]
F_rec [in ABS.abs_defs]
F_ind [in ABS.abs_defs]
F_rect [in ABS.abs_defs]
G
G [in ABS.abs_defs]get_type [in ABS.abs_functional_metatheory]
get_class_decl [in ABS.abs_imp]
get_method_decl [in ABS.abs_imp]
get_type [in ABS.abs_imp]
get_params [in ABS.abs_imp]
get_methods [in ABS.abs_imp]
get_fields [in ABS.abs_imp]
get_class_name [in ABS.abs_imp]
G_vdash_s [in ABS.abs_functional_metatheory]
I
i [in ABS.abs_defs]L
local_well_typed [in ABS.abs_functional_metatheory]M
m [in ABS.abs_defs]M_sind [in ABS.abs_defs]
M_rec [in ABS.abs_defs]
M_ind [in ABS.abs_defs]
M_rect [in ABS.abs_defs]
O
o [in ABS.abs_defs]P
P_sind [in ABS.abs_defs]P_rec [in ABS.abs_defs]
P_ind [in ABS.abs_defs]
P_rect [in ABS.abs_defs]
Q
queue [in ABS.abs_defs]queue_well_typed [in ABS.abs_imperative_metatheory]
R
reduce [in ABS.abs_functional_metatheory]red_e_sind [in ABS.abs_defs]
red_e_ind [in ABS.abs_defs]
remove [in ABS.abs_imp]
replace_var [in ABS.abs_util]
rhs_sind [in ABS.abs_defs]
rhs_rec [in ABS.abs_defs]
rhs_ind [in ABS.abs_defs]
rhs_rect [in ABS.abs_defs]
S
s [in ABS.abs_defs]sig_sind [in ABS.abs_defs]
sig_rec [in ABS.abs_defs]
sig_ind [in ABS.abs_defs]
sig_rect [in ABS.abs_defs]
stmt_step_sind [in ABS.abs_imp]
stmt_step_ind [in ABS.abs_imp]
stmt_sind [in ABS.abs_defs]
stmt_rec [in ABS.abs_defs]
stmt_ind [in ABS.abs_defs]
stmt_rect [in ABS.abs_defs]
stmt_well_typed_sind [in ABS.abs_imperative_metatheory]
stmt_well_typed_ind [in ABS.abs_imperative_metatheory]
sub_well_typed [in ABS.abs_util]
T
tasko [in ABS.abs_defs]task_sind [in ABS.abs_defs]
task_rec [in ABS.abs_defs]
task_ind [in ABS.abs_defs]
task_rect [in ABS.abs_defs]
to [in ABS.abs_defs]
typ_es [in ABS.abs_util]
typ_F_sind [in ABS.abs_defs]
typ_F_ind [in ABS.abs_defs]
typ_e_sind [in ABS.abs_defs]
typ_e_ind [in ABS.abs_defs]
T_sind [in ABS.abs_defs]
T_rec [in ABS.abs_defs]
T_ind [in ABS.abs_defs]
T_rect [in ABS.abs_defs]
t_sind [in ABS.abs_defs]
t_rec [in ABS.abs_defs]
t_ind [in ABS.abs_defs]
t_rect [in ABS.abs_defs]
W
well_formed [in ABS.abs_defs]X
x [in ABS.abs_defs]Z
z [in ABS.abs_defs]| 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 | (397 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 | (1 entry) |
| 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 | (32 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 | (7 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 | (105 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 | (94 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 | (23 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 | (6 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 | (6 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 | (1 entry) |
| 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 | (122 entries) |