| 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 | (170 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 | (4 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 | (3 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 | (9 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 | (4 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 | (64 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 | (19 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 | (9 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 | (4 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 | (54 entries) |
Global Index
A
abs_functional_metatheory [library]abs_defs [library]
abs_examples [library]
B
b [definition, in ABS.abs_defs]C
combine_map [lemma, in ABS.utils]combine_app [lemma, in ABS.utils]
combine_snd [lemma, in ABS.utils]
combine_nil [lemma, in ABS.utils]
combine_fst [lemma, in ABS.utils]
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_sig [constructor, in ABS.abs_defs]
ctxv_T [constructor, in ABS.abs_defs]
D
disjoint [definition, in ABS.abs_defs]disjoint_monotone [lemma, in ABS.utils]
disjoint_empty [lemma, in ABS.utils]
E
e [inductive, in ABS.abs_defs]eq_z [lemma, in ABS.abs_defs]
eq_b [lemma, in ABS.abs_defs]
eq_x [lemma, in ABS.abs_defs]
eq_fn [lemma, in ABS.abs_defs]
eq_i [lemma, in ABS.abs_defs]
e_list_fresh [lemma, in ABS.utils]
e_list_subst [lemma, in ABS.utils]
e_list_subst_map [lemma, in ABS.utils]
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_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_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_list_e [variable, in ABS.abs_defs]
e_rect.P_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_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]fn [definition, in ABS.abs_defs]
fold_add_comm [lemma, in ABS.utils]
fold_not_in [lemma, in ABS.utils]
fold_map_reshuffle [lemma, in ABS.utils]
fold_map3 [lemma, in ABS.utils]
fold_map2 [lemma, in ABS.utils]
fold_map1 [lemma, in ABS.utils]
fold_map [lemma, in ABS.utils]
fold_map5 [lemma, in ABS.abs_functional_metatheory]
fold_map4 [lemma, in ABS.abs_functional_metatheory]
fresh_var_subst [lemma, in ABS.utils]
fresh_monotone_el [lemma, in ABS.utils]
fresh_first_el [lemma, in ABS.utils]
fresh_monotone_e [lemma, in ABS.utils]
fresh_first_e [lemma, in ABS.utils]
fresh_consistent [lemma, in ABS.abs_functional_metatheory]
fresh_subG [lemma, in ABS.abs_functional_metatheory]
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]
FunctionalMetatheory [section, in ABS.abs_functional_metatheory]
FunctionalMetatheory.vars_well_typed [variable, in ABS.abs_functional_metatheory]
FunctionalMetatheory.vars_fs_distinct [variable, in ABS.abs_functional_metatheory]
_ G⊢ _ [notation, in ABS.abs_functional_metatheory]
_ ⊆ _ [notation, in ABS.abs_functional_metatheory]
_ F⊢ _ [notation, in ABS.abs_functional_metatheory]
_ ⊢ _ : _ [notation, in ABS.abs_functional_metatheory]
func_const_5 [definition, in ABS.abs_examples]
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]G_vdash_s [definition, in ABS.abs_functional_metatheory]
I
i [definition, in ABS.abs_defs]in_fst_iff [lemma, in ABS.utils]
in_combine_split [lemma, in ABS.utils]
in_split [lemma, in ABS.utils]
in_combine [lemma, in ABS.utils]
L
ListLemmas [section, in ABS.utils]M
Map [module, in ABS.abs_defs]MapFacts [module, in ABS.utils]
MapFacts [module, in ABS.abs_functional_metatheory]
MapLemmas [section, in ABS.utils]
map_add_comm [lemma, in ABS.utils]
map_neq_none_is_some [lemma, in ABS.utils]
map_split' [lemma, in ABS.utils]
map_xs [lemma, in ABS.utils]
map_split [lemma, in ABS.utils]
map_eq [lemma, in ABS.utils]
P
pat2_id [lemma, in ABS.utils]R
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_var [constructor, in ABS.abs_defs]
red_e [inductive, in ABS.abs_defs]
replace_var [definition, in ABS.utils]
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.utils]
split_corresponding_list [lemma, in ABS.utils]
subG [definition, in ABS.abs_functional_metatheory]
subG_type [lemma, in ABS.abs_functional_metatheory]
subG_consistent [lemma, in ABS.abs_functional_metatheory]
subG_add_2 [lemma, in ABS.abs_functional_metatheory]
subG_add [lemma, in ABS.abs_functional_metatheory]
subG_refl [lemma, in ABS.abs_functional_metatheory]
subst_fn [lemma, in ABS.utils]
subst_var [lemma, in ABS.utils]
subst_term [lemma, in ABS.utils]
subst_snd_commutes [lemma, in ABS.utils]
subst_fst_commute [lemma, in ABS.utils]
subst_lemma [lemma, in ABS.abs_functional_metatheory]
subst_lemma_one [lemma, in ABS.abs_functional_metatheory]
subst_lemma_one_alt [lemma, in ABS.abs_functional_metatheory]
T
t [inductive, in ABS.abs_defs]T [inductive, in ABS.abs_defs]
type_preservation [lemma, in ABS.abs_functional_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_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_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]
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_b [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_int [constructor, in ABS.abs_defs]
T_bool [constructor, in ABS.abs_defs]
U
utils [library]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]_ ⊆ _ [in ABS.abs_functional_metatheory]
_ F⊢ _ [in ABS.abs_functional_metatheory]
_ ⊢ _ : _ [in ABS.abs_functional_metatheory]
Module Index
M
Map [in ABS.abs_defs]MapFacts [in ABS.utils]
MapFacts [in ABS.abs_functional_metatheory]
Variable Index
E
e_rect.H_list_e_cons [in ABS.abs_defs]e_rect.H_list_e_nil [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_list_e [in ABS.abs_defs]
e_rect.P_e [in ABS.abs_defs]
F
FunctionalMetatheory.vars_well_typed [in ABS.abs_functional_metatheory]FunctionalMetatheory.vars_fs_distinct [in ABS.abs_functional_metatheory]
Library Index
A
abs_functional_metatheoryabs_defs
abs_examples
U
utilsLemma Index
C
combine_map [in ABS.utils]combine_app [in ABS.utils]
combine_snd [in ABS.utils]
combine_nil [in ABS.utils]
combine_fst [in ABS.utils]
D
disjoint_monotone [in ABS.utils]disjoint_empty [in ABS.utils]
E
eq_z [in ABS.abs_defs]eq_b [in ABS.abs_defs]
eq_x [in ABS.abs_defs]
eq_fn [in ABS.abs_defs]
eq_i [in ABS.abs_defs]
e_list_fresh [in ABS.utils]
e_list_subst [in ABS.utils]
e_list_subst_map [in ABS.utils]
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]
F
fold_add_comm [in ABS.utils]fold_not_in [in ABS.utils]
fold_map_reshuffle [in ABS.utils]
fold_map3 [in ABS.utils]
fold_map2 [in ABS.utils]
fold_map1 [in ABS.utils]
fold_map [in ABS.utils]
fold_map5 [in ABS.abs_functional_metatheory]
fold_map4 [in ABS.abs_functional_metatheory]
fresh_var_subst [in ABS.utils]
fresh_monotone_el [in ABS.utils]
fresh_first_el [in ABS.utils]
fresh_monotone_e [in ABS.utils]
fresh_first_e [in ABS.utils]
fresh_consistent [in ABS.abs_functional_metatheory]
fresh_subG [in ABS.abs_functional_metatheory]
I
in_fst_iff [in ABS.utils]in_combine_split [in ABS.utils]
in_split [in ABS.utils]
in_combine [in ABS.utils]
M
map_add_comm [in ABS.utils]map_neq_none_is_some [in ABS.utils]
map_split' [in ABS.utils]
map_xs [in ABS.utils]
map_split [in ABS.utils]
map_eq [in ABS.utils]
P
pat2_id [in ABS.utils]S
same_type_sub [in ABS.abs_functional_metatheory]split_corresponding_list_no_length [in ABS.utils]
split_corresponding_list [in ABS.utils]
subG_type [in ABS.abs_functional_metatheory]
subG_consistent [in ABS.abs_functional_metatheory]
subG_add_2 [in ABS.abs_functional_metatheory]
subG_add [in ABS.abs_functional_metatheory]
subG_refl [in ABS.abs_functional_metatheory]
subst_fn [in ABS.utils]
subst_var [in ABS.utils]
subst_term [in ABS.utils]
subst_snd_commutes [in ABS.utils]
subst_fst_commute [in ABS.utils]
subst_lemma [in ABS.abs_functional_metatheory]
subst_lemma_one [in ABS.abs_functional_metatheory]
subst_lemma_one_alt [in ABS.abs_functional_metatheory]
T
type_preservation [in ABS.abs_functional_metatheory]typ_e_G_Equal_equiv [in ABS.abs_functional_metatheory]
typ_e_G_Equal_equiv_imp [in ABS.abs_functional_metatheory]
Constructor Index
C
ctxv_sig [in ABS.abs_defs]ctxv_T [in ABS.abs_defs]
E
e_fn_call [in ABS.abs_defs]e_var [in ABS.abs_defs]
e_t [in ABS.abs_defs]
F
F_fn [in ABS.abs_defs]R
red_fun_ground [in ABS.abs_defs]red_fun_exp [in ABS.abs_defs]
red_var [in ABS.abs_defs]
S
sig_sig [in ABS.abs_defs]T
typ_func_decl [in ABS.abs_defs]typ_func_expr [in ABS.abs_defs]
typ_var [in ABS.abs_defs]
typ_int [in ABS.abs_defs]
typ_bool [in ABS.abs_defs]
t_int [in ABS.abs_defs]
t_b [in ABS.abs_defs]
T_int [in ABS.abs_defs]
T_bool [in ABS.abs_defs]
Inductive Index
C
ctxv [in ABS.abs_defs]E
e [in ABS.abs_defs]F
F [in ABS.abs_defs]R
red_e [in ABS.abs_defs]S
sig [in ABS.abs_defs]T
t [in ABS.abs_defs]T [in ABS.abs_defs]
typ_F [in ABS.abs_defs]
typ_e [in ABS.abs_defs]
Section Index
E
e_rect [in ABS.abs_defs]F
FunctionalMetatheory [in ABS.abs_functional_metatheory]L
ListLemmas [in ABS.utils]M
MapLemmas [in ABS.utils]Definition Index
B
b [in ABS.abs_defs]C
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
disjoint [in ABS.abs_defs]E
e_call_const_5 [in ABS.abs_examples]e_const_5 [in ABS.abs_examples]
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
fn [in ABS.abs_defs]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]
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]G_vdash_s [in ABS.abs_functional_metatheory]
I
i [in ABS.abs_defs]R
red_e_sind [in ABS.abs_defs]red_e_ind [in ABS.abs_defs]
replace_var [in ABS.utils]
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]
subG [in ABS.abs_functional_metatheory]
T
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 | (170 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 | (4 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 | (3 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 | (9 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 | (4 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 | (64 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 | (19 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 | (9 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 | (4 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 | (54 entries) |