| 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 | _ | (756 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 | _ | (8 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 | _ | (416 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 | _ | (197 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 | _ | (46 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 | _ | (57 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 | _ | (13 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 | _ | (19 entries) |
Global Index
A
abs [constructor, in STLC_Solutions]abs [constructor, in STLC_Tutorial]
AdditionalTactics [library]
app [constructor, in STLC_Solutions]
app [constructor, in STLC_Tutorial]
ATOM [module, in Atom]
atom [axiom, in Atom]
Atom [library]
AtomImpl [module, in Atom]
AtomSet [module, in Atom]
ATOM.Atom_as_OT.AtomSet.atom_fresh_for_set [lemma, in Atom]
ATOM.Atom_as_OT.AtomSet.example_pick_fresh_use [lemma, in Atom]
ATOM.Atom_as_OT.t [definition, in Atom]
Atom_as_OT [module, in Atom]
atom_fresh_for_list [axiom, in Atom]
auto_example [lemma, in CoqIntro]
B
binding [inductive, in Fsub_LetSum_Definitions]binding [inductive, in Fsub_Definitions]
binds [definition, in Environment]
binds_concat_inv [lemma, in Environment]
binds_concat_ok [lemma, in Environment]
binds_fresh [lemma, in Environment]
binds_head [lemma, in Environment]
binds_In [lemma, in Environment]
binds_map [lemma, in Environment]
binds_mid [lemma, in Environment]
binds_mid_eq [lemma, in Environment]
binds_mid_eq_cons [lemma, in Environment]
binds_remove_mid [lemma, in Environment]
binds_remove_mid_cons [lemma, in Environment]
binds_singleton [lemma, in Environment]
binds_singleton_inv [lemma, in Environment]
binds_tail [lemma, in Environment]
binds_weaken [lemma, in Environment]
binds_weaken_at_head [lemma, in Environment]
bind_sub [constructor, in Fsub_LetSum_Definitions]
bind_sub [constructor, in Fsub_Definitions]
bind_typ [constructor, in Fsub_Definitions]
bind_typ [constructor, in Fsub_LetSum_Definitions]
body_e [definition, in Fsub_LetSum_Definitions]
body_from_expr_let [lemma, in Fsub_LetSum_Infrastructure]
body_inl_from_expr_case [lemma, in Fsub_LetSum_Infrastructure]
body_inr_from_expr_case [lemma, in Fsub_LetSum_Infrastructure]
bool_option [inductive, in CoqIntro]
bool_tm_bool [lemma, in CoqIntro]
bool_to_tm [definition, in CoqIntro]
bvalue [inductive, in CoqIntro]
bvar [constructor, in STLC_Tutorial]
bvar [constructor, in STLC_Solutions]
b_false [constructor, in CoqIntro]
b_true [constructor, in CoqIntro]
C
canonical_form_abs [lemma, in Fsub_Soundness]canonical_form_abs [lemma, in Fsub_LetSum_Soundness]
canonical_form_sum [lemma, in Fsub_LetSum_Soundness]
canonical_form_tabs [lemma, in Fsub_LetSum_Soundness]
canonical_form_tabs [lemma, in Fsub_Soundness]
concat_assoc [lemma, in Environment]
concat_nil [lemma, in Environment]
cons_concat [lemma, in Environment]
cons_concat_assoc [lemma, in Environment]
contradictory_equalities_exercise [lemma, in CoqIntro]
contradictory_equalities_exercise_sol [lemma, in CoqIntro]
CoqIntro [library]
D
Decide [module, in FSetDecide]Decide.FSetDecideAuxiliary.dec_eq [lemma, in FSetDecide]
Decide.FSetDecideAuxiliary.dec_In [lemma, in FSetDecide]
Decide.FSetDecideAuxiliary.elt_FSet_Prop [constructor, in FSetDecide]
Decide.FSetDecideAuxiliary.Empty_FSet_Prop [constructor, in FSetDecide]
Decide.FSetDecideAuxiliary.Equal_FSet_Prop [constructor, in FSetDecide]
Decide.FSetDecideAuxiliary.eq_elt_prop [constructor, in FSetDecide]
Decide.FSetDecideAuxiliary.eq_Prop [constructor, in FSetDecide]
Decide.FSetDecideAuxiliary.FSet_elt_Prop [inductive, in FSetDecide]
Decide.FSetDecideAuxiliary.FSet_Prop [inductive, in FSetDecide]
Decide.FSetDecideAuxiliary.Subset_FSet_Prop [constructor, in FSetDecide]
Decide.FSetDecideTestCases.eq_chain_test [lemma, in FSetDecide]
Decide.FSetDecideTestCases.function_test_1 [lemma, in FSetDecide]
Decide.FSetDecideTestCases.function_test_2 [lemma, in FSetDecide]
Decide.FSetDecideTestCases.test_eq_disjunction [lemma, in FSetDecide]
Decide.FSetDecideTestCases.test_eq_neq_trans_1 [lemma, in FSetDecide]
Decide.FSetDecideTestCases.test_eq_neq_trans_2 [lemma, in FSetDecide]
Decide.FSetDecideTestCases.test_eq_trans_1 [lemma, in FSetDecide]
Decide.FSetDecideTestCases.test_eq_trans_2 [lemma, in FSetDecide]
Decide.FSetDecideTestCases.test_iff_conj [lemma, in FSetDecide]
Decide.FSetDecideTestCases.test_In_singleton [lemma, in FSetDecide]
Decide.FSetDecideTestCases.test_not_In_conj [lemma, in FSetDecide]
Decide.FSetDecideTestCases.test_not_In_disj [lemma, in FSetDecide]
Decide.FSetDecideTestCases.test_set_ops_1 [lemma, in FSetDecide]
Decide.FSetDecideTestCases.test_Subset_add_remove [lemma, in FSetDecide]
Decide.FSetDecideTestCases.test_too_complex [lemma, in FSetDecide]
Decide.FSetLogicalFacts.contrapositive [lemma, in FSetDecide]
Decide.FSetLogicalFacts.dec_iff [lemma, in FSetDecide]
Decide.FSetLogicalFacts.imp_not_l [lemma, in FSetDecide]
Decide.FSetLogicalFacts.not_and_iff [lemma, in FSetDecide]
Decide.FSetLogicalFacts.not_false_iff [lemma, in FSetDecide]
Decide.FSetLogicalFacts.not_imp_iff [lemma, in FSetDecide]
Decide.FSetLogicalFacts.not_imp_rev_iff [lemma, in FSetDecide]
Decide.FSetLogicalFacts.not_not_iff [lemma, in FSetDecide]
Decide.FSetLogicalFacts.not_or_iff [lemma, in FSetDecide]
Decide.FSetLogicalFacts.not_true_iff [lemma, in FSetDecide]
Decide.FSetLogicalFacts.or_not_l_iff_1 [lemma, in FSetDecide]
Decide.FSetLogicalFacts.or_not_l_iff_2 [lemma, in FSetDecide]
Decide.FSetLogicalFacts.or_not_r_iff_1 [lemma, in FSetDecide]
Decide.FSetLogicalFacts.or_not_r_iff_2 [lemma, in FSetDecide]
Decide.FSetLogicalFacts.test_pull [lemma, in FSetDecide]
Decide.FSetLogicalFacts.test_push [lemma, in FSetDecide]
demo_open [lemma, in STLC_Tutorial]
demo_open [lemma, in STLC_Solutions]
demo_rep1 [definition, in STLC_Solutions]
demo_rep1 [definition, in STLC_Tutorial]
demo_rep2 [definition, in STLC_Solutions]
demo_rep2 [definition, in STLC_Tutorial]
demo_subst1 [lemma, in STLC_Solutions]
demo_subst1 [lemma, in STLC_Tutorial]
destruct_example [lemma, in CoqIntro]
destruct_negation_example [lemma, in CoqIntro]
dom [definition, in Environment]
dom_concat [lemma, in Environment]
dom_map [lemma, in Environment]
dom_nil [lemma, in Environment]
dom_push [lemma, in Environment]
dom_single [lemma, in Environment]
dom_singleton_list [lemma, in Environment]
E
E [module, in FiniteSets]eauto_example [lemma, in CoqIntro]
eauto_using_example [lemma, in CoqIntro]
elim_incl_app [lemma, in ListFacts]
elim_incl_cons [lemma, in ListFacts]
elim_not_In_app [lemma, in ListFacts]
elim_not_In_cons [lemma, in ListFacts]
Environment [library]
equality_example_1 [lemma, in CoqIntro]
equality_example_2a [lemma, in CoqIntro]
equality_example_2b [lemma, in CoqIntro]
equality_example_2c [lemma, in CoqIntro]
equality_example_3 [lemma, in CoqIntro]
equality_example_4 [lemma, in CoqIntro]
equality_exercise [lemma, in CoqIntro]
equality_exercise_sol [lemma, in CoqIntro]
eq_atom_dec [axiom, in Atom]
eq_if_Equal [axiom, in FiniteSets]
eq_rect_eq_list [lemma, in ListFacts]
eval [inductive, in STLC_Tutorial]
eval [inductive, in CoqIntro]
eval [inductive, in STLC_Solutions]
eval_app_1 [constructor, in STLC_Tutorial]
eval_app_1 [constructor, in STLC_Solutions]
eval_app_2 [constructor, in STLC_Solutions]
eval_app_2 [constructor, in STLC_Tutorial]
eval_beta [constructor, in STLC_Solutions]
eval_beta [constructor, in STLC_Tutorial]
eval_deterministic [lemma, in CoqIntro]
eval_deterministic_sol [lemma, in CoqIntro]
eval_fact_exercise [lemma, in CoqIntro]
eval_fact_exercise_sol [lemma, in CoqIntro]
eval_full_eval_sol [lemma, in CoqIntro]
eval_many [inductive, in CoqIntro]
eval_many_rtc_sol [lemma, in CoqIntro]
eval_regular [lemma, in STLC_Tutorial]
eval_regular [lemma, in STLC_Solutions]
eval_rtc [inductive, in CoqIntro]
eval_rtc_many_sol [lemma, in CoqIntro]
exists_iszero_nvalue [lemma, in CoqIntro]
exists_iszero_nvalue_sol [lemma, in CoqIntro]
exists_pred_zero [lemma, in CoqIntro]
exp [inductive, in Fsub_Definitions]
exp [inductive, in STLC_Tutorial]
exp [inductive, in STLC_Solutions]
exp [inductive, in Fsub_LetSum_Definitions]
expr [inductive, in Fsub_LetSum_Definitions]
expr [inductive, in Fsub_Definitions]
expr_abs [constructor, in Fsub_LetSum_Definitions]
expr_abs [constructor, in Fsub_Definitions]
expr_app [constructor, in Fsub_LetSum_Definitions]
expr_app [constructor, in Fsub_Definitions]
expr_case [constructor, in Fsub_LetSum_Definitions]
expr_case_from_body [lemma, in Fsub_LetSum_Infrastructure]
expr_inl [constructor, in Fsub_LetSum_Definitions]
expr_inr [constructor, in Fsub_LetSum_Definitions]
expr_let [constructor, in Fsub_LetSum_Definitions]
expr_let_from_body [lemma, in Fsub_LetSum_Infrastructure]
expr_tabs [constructor, in Fsub_LetSum_Definitions]
expr_tabs [constructor, in Fsub_Definitions]
expr_tapp [constructor, in Fsub_LetSum_Definitions]
expr_tapp [constructor, in Fsub_Definitions]
expr_var [constructor, in Fsub_Definitions]
expr_var [constructor, in Fsub_LetSum_Definitions]
exp_abs [constructor, in Fsub_Definitions]
exp_abs [constructor, in Fsub_LetSum_Definitions]
exp_app [constructor, in Fsub_Definitions]
exp_app [constructor, in Fsub_LetSum_Definitions]
exp_bvar [constructor, in Fsub_LetSum_Definitions]
exp_bvar [constructor, in Fsub_Definitions]
exp_case [constructor, in Fsub_LetSum_Definitions]
exp_fvar [constructor, in Fsub_LetSum_Definitions]
exp_fvar [constructor, in Fsub_Definitions]
exp_inl [constructor, in Fsub_LetSum_Definitions]
exp_inr [constructor, in Fsub_LetSum_Definitions]
exp_let [constructor, in Fsub_LetSum_Definitions]
exp_tabs [constructor, in Fsub_Definitions]
exp_tabs [constructor, in Fsub_LetSum_Definitions]
exp_tapp [constructor, in Fsub_LetSum_Definitions]
exp_tapp [constructor, in Fsub_Definitions]
e_if [constructor, in CoqIntro]
e_iffalse [constructor, in CoqIntro]
e_iftrue [constructor, in CoqIntro]
e_if_true_or_false [lemma, in CoqIntro]
e_iszero [constructor, in CoqIntro]
e_iszerosucc [constructor, in CoqIntro]
e_iszerozero [constructor, in CoqIntro]
e_iszero_nvalue [lemma, in CoqIntro]
e_pred [constructor, in CoqIntro]
e_predsucc [constructor, in CoqIntro]
e_predzero [constructor, in CoqIntro]
e_succ [constructor, in CoqIntro]
e_succ_pred_succ [lemma, in CoqIntro]
F
F [module, in FiniteSets]False_hypothesis [lemma, in CoqIntro]
FiniteSets [library]
fresh_mid_head [lemma, in Environment]
fresh_mid_tail [lemma, in Environment]
FSetDecide [library]
FSetDecideAuxiliary [module, in FSetDecide]
FSetDecideTestCases [module, in FSetDecide]
FSetLogicalFacts [module, in FSetDecide]
FSetNotin [library]
Fsub_Definitions [library]
Fsub_Infrastructure [library]
Fsub_Lemmas [library]
Fsub_LetSum_Definitions [library]
Fsub_LetSum_Infrastructure [library]
Fsub_LetSum_Lemmas [library]
Fsub_LetSum_Soundness [library]
Fsub_Soundness [library]
full_eval [inductive, in CoqIntro]
full_eval_complete_sol [lemma, in CoqIntro]
full_eval_from_value_sol [lemma, in CoqIntro]
full_eval_to_value_sol [lemma, in CoqIntro]
fv [definition, in STLC_Tutorial]
fv [definition, in STLC_Solutions]
fvar [constructor, in STLC_Tutorial]
fvar [constructor, in STLC_Solutions]
fv_ee [definition, in Fsub_Infrastructure]
fv_ee [definition, in Fsub_LetSum_Infrastructure]
fv_te [definition, in Fsub_LetSum_Infrastructure]
fv_te [definition, in Fsub_Infrastructure]
fv_tt [definition, in Fsub_LetSum_Infrastructure]
fv_tt [definition, in Fsub_Infrastructure]
f_iffalse [constructor, in CoqIntro]
f_iftrue [constructor, in CoqIntro]
f_iszerosucc [constructor, in CoqIntro]
f_iszerozero [constructor, in CoqIntro]
f_predsucc [constructor, in CoqIntro]
f_predzero [constructor, in CoqIntro]
f_succ [constructor, in CoqIntro]
f_value [constructor, in CoqIntro]
G
get [definition, in Environment]I
if_bvalue [lemma, in CoqIntro]InA_iff_In [lemma, in ListFacts]
incl_nil [lemma, in ListFacts]
incl_trans [lemma, in ListFacts]
interp [definition, in CoqIntro]
interp_fully_reduces_sol [lemma, in CoqIntro]
interp_reduces_sol [lemma, in CoqIntro]
inversion_exercise [lemma, in CoqIntro]
inversion_exercise_sol [lemma, in CoqIntro]
In_incl [lemma, in ListFacts]
is_bool [definition, in CoqIntro]
L
lc [inductive, in STLC_Tutorial]lc [inductive, in STLC_Solutions]
lc_abs [constructor, in STLC_Solutions]
lc_abs [constructor, in STLC_Tutorial]
lc_app [constructor, in STLC_Tutorial]
lc_app [constructor, in STLC_Solutions]
lc_var [constructor, in STLC_Solutions]
lc_var [constructor, in STLC_Tutorial]
lelistA_dec [lemma, in ListFacts]
lelistA_unique [lemma, in ListFacts]
ListFacts [library]
M
Make [module, in FiniteSets]map [definition, in Environment]
map_concat [lemma, in Environment]
map_nil [lemma, in Environment]
map_push [lemma, in Environment]
map_single [lemma, in Environment]
map_singleton_list [lemma, in Environment]
map_subst_tb_id [lemma, in Fsub_Lemmas]
map_subst_tb_id [lemma, in Fsub_LetSum_Lemmas]
Metatheory [library]
m_if [lemma, in CoqIntro]
m_iftrue_step [lemma, in CoqIntro]
m_iftrue_step_sol [lemma, in CoqIntro]
m_if_iszero_conj [lemma, in CoqIntro]
m_if_iszero_conj_sol [lemma, in CoqIntro]
m_iszero [lemma, in CoqIntro]
m_iszero_nvalue [lemma, in CoqIntro]
m_one [lemma, in CoqIntro]
m_one_sol [lemma, in CoqIntro]
m_pred [lemma, in CoqIntro]
m_pred_sol [lemma, in CoqIntro]
m_refl [constructor, in CoqIntro]
m_step [constructor, in CoqIntro]
m_succ [lemma, in CoqIntro]
m_succ_pred_succ [lemma, in CoqIntro]
m_succ_pred_succ_alt [lemma, in CoqIntro]
m_succ_sol [lemma, in CoqIntro]
m_three [lemma, in CoqIntro]
m_three_conj [lemma, in CoqIntro]
m_trans [lemma, in CoqIntro]
m_trans_sol [lemma, in CoqIntro]
m_two [lemma, in CoqIntro]
m_two_conj [lemma, in CoqIntro]
m_two_exists [lemma, in CoqIntro]
m_two_exists' [lemma, in CoqIntro]
m_two_exists'' [lemma, in CoqIntro]
m_two_sol [lemma, in CoqIntro]
N
nat_option [inductive, in CoqIntro]nat_tm_nat [lemma, in CoqIntro]
nat_to_tm [definition, in CoqIntro]
negation_exercise [lemma, in CoqIntro]
negation_exercise_sol [lemma, in CoqIntro]
nil_concat [lemma, in Environment]
normal_form [definition, in CoqIntro]
normal_form_from_forall [lemma, in CoqIntro]
normal_form_from_forall_sol [lemma, in CoqIntro]
normal_form_if [lemma, in CoqIntro]
normal_form_if_sol [lemma, in CoqIntro]
normal_form_succ [lemma, in CoqIntro]
normal_form_to_forall [lemma, in CoqIntro]
normal_form_to_forall_sol [lemma, in CoqIntro]
Notin [module, in FSetNotin]
Notin.elim_notin_singleton [lemma, in FSetNotin]
Notin.elim_notin_singleton' [lemma, in FSetNotin]
Notin.elim_notin_union [lemma, in FSetNotin]
Notin.in_singleton [lemma, in FSetNotin]
Notin.notin_empty [lemma, in FSetNotin]
Notin.notin_singleton [lemma, in FSetNotin]
Notin.notin_singleton_rw [lemma, in FSetNotin]
Notin.notin_singleton_swap [lemma, in FSetNotin]
Notin.notin_union [lemma, in FSetNotin]
Notin.test_notin_solve_1 [lemma, in FSetNotin]
Notin.test_notin_solve_2 [lemma, in FSetNotin]
Notin.test_notin_solve_3 [lemma, in FSetNotin]
Notin.test_notin_solve_4 [lemma, in FSetNotin]
Notin.test_notin_solve_5 [lemma, in FSetNotin]
notin_fv_tt_open [lemma, in Fsub_LetSum_Lemmas]
notin_fv_tt_open [lemma, in Fsub_Lemmas]
notin_fv_wf [lemma, in Fsub_LetSum_Lemmas]
notin_fv_wf [lemma, in Fsub_Lemmas]
not_InA_if_Sort_Inf [lemma, in ListFacts]
not_In_app [lemma, in ListFacts]
not_in_cons [lemma, in ListFacts]
no_bool [constructor, in CoqIntro]
no_nat [constructor, in CoqIntro]
nvalue [inductive, in CoqIntro]
nvalue_is_normal_form [lemma, in CoqIntro]
nvalue_is_normal_form' [lemma, in CoqIntro]
n_succ [constructor, in CoqIntro]
n_zero [constructor, in CoqIntro]
O
ok [inductive, in Environment]ok_cons [constructor, in Environment]
ok_from_wf_env [lemma, in Fsub_Lemmas]
ok_from_wf_env [lemma, in Fsub_LetSum_Lemmas]
ok_map [lemma, in Environment]
ok_map_app_l [lemma, in Environment]
ok_nil [constructor, in Environment]
ok_push [lemma, in Environment]
ok_remove_mid [lemma, in Environment]
ok_remove_mid_cons [lemma, in Environment]
ok_singleton [lemma, in Environment]
open [definition, in STLC_Tutorial]
open [definition, in STLC_Solutions]
open_abs [lemma, in STLC_Solutions]
open_abs [lemma, in STLC_Tutorial]
open_ee [definition, in Fsub_LetSum_Definitions]
open_ee [definition, in Fsub_Definitions]
open_ee_body_e [lemma, in Fsub_LetSum_Infrastructure]
open_ee_rec [definition, in Fsub_LetSum_Definitions]
open_ee_rec [definition, in Fsub_Definitions]
open_ee_rec_expr [lemma, in Fsub_Infrastructure]
open_ee_rec_expr [lemma, in Fsub_LetSum_Infrastructure]
open_ee_rec_expr_aux [lemma, in Fsub_Infrastructure]
open_ee_rec_expr_aux [lemma, in Fsub_LetSum_Infrastructure]
open_ee_rec_type_aux [lemma, in Fsub_Infrastructure]
open_ee_rec_type_aux [lemma, in Fsub_LetSum_Infrastructure]
open_rec [definition, in STLC_Solutions]
open_rec [definition, in STLC_Tutorial]
open_rec_lc [lemma, in STLC_Tutorial]
open_rec_lc [lemma, in STLC_Solutions]
open_rec_lc_core [lemma, in STLC_Tutorial]
open_rec_lc_core [lemma, in STLC_Solutions]
open_rec_lc_0 [lemma, in STLC_Solutions]
open_rec_lc_0 [lemma, in STLC_Tutorial]
open_rec_lc_1 [lemma, in STLC_Tutorial]
open_rec_lc_1 [lemma, in STLC_Solutions]
open_te [definition, in Fsub_LetSum_Definitions]
open_te [definition, in Fsub_Definitions]
open_te_rec [definition, in Fsub_Definitions]
open_te_rec [definition, in Fsub_LetSum_Definitions]
open_te_rec_expr [lemma, in Fsub_Infrastructure]
open_te_rec_expr [lemma, in Fsub_LetSum_Infrastructure]
open_te_rec_expr_aux [lemma, in Fsub_LetSum_Infrastructure]
open_te_rec_expr_aux [lemma, in Fsub_Infrastructure]
open_te_rec_type_aux [lemma, in Fsub_LetSum_Infrastructure]
open_te_rec_type_aux [lemma, in Fsub_Infrastructure]
open_tt [definition, in Fsub_Definitions]
open_tt [definition, in Fsub_LetSum_Definitions]
open_tt_rec [definition, in Fsub_LetSum_Definitions]
open_tt_rec [definition, in Fsub_Definitions]
open_tt_rec_type [lemma, in Fsub_Infrastructure]
open_tt_rec_type [lemma, in Fsub_LetSum_Infrastructure]
open_tt_rec_type_aux [lemma, in Fsub_Infrastructure]
open_tt_rec_type_aux [lemma, in Fsub_LetSum_Infrastructure]
P
pred_not_circular [lemma, in CoqIntro]pred_not_circular_sol [lemma, in CoqIntro]
preservation [lemma, in Fsub_Soundness]
preservation [lemma, in STLC_Tutorial]
preservation [lemma, in Fsub_LetSum_Soundness]
preservation [lemma, in STLC_Solutions]
progress [lemma, in STLC_Solutions]
progress [lemma, in Fsub_Soundness]
progress [lemma, in STLC_Tutorial]
progress [lemma, in Fsub_LetSum_Soundness]
R
red [inductive, in Fsub_Definitions]red [inductive, in Fsub_LetSum_Definitions]
red_abs [constructor, in Fsub_LetSum_Definitions]
red_abs [constructor, in Fsub_Definitions]
red_app_1 [constructor, in Fsub_LetSum_Definitions]
red_app_1 [constructor, in Fsub_Definitions]
red_app_2 [constructor, in Fsub_Definitions]
red_app_2 [constructor, in Fsub_LetSum_Definitions]
red_case_inl [constructor, in Fsub_LetSum_Definitions]
red_case_inr [constructor, in Fsub_LetSum_Definitions]
red_case_1 [constructor, in Fsub_LetSum_Definitions]
red_inl_1 [constructor, in Fsub_LetSum_Definitions]
red_inr_1 [constructor, in Fsub_LetSum_Definitions]
red_let [constructor, in Fsub_LetSum_Definitions]
red_let_1 [constructor, in Fsub_LetSum_Definitions]
red_regular [lemma, in Fsub_LetSum_Lemmas]
red_regular [lemma, in Fsub_Lemmas]
red_tabs [constructor, in Fsub_Definitions]
red_tabs [constructor, in Fsub_LetSum_Definitions]
red_tapp [constructor, in Fsub_Definitions]
red_tapp [constructor, in Fsub_LetSum_Definitions]
remember_example [lemma, in CoqIntro]
r_eval [constructor, in CoqIntro]
r_refl [constructor, in CoqIntro]
r_trans [constructor, in CoqIntro]
S
S [module, in FiniteSets]singleton_list [definition, in Environment]
single_step_to_multi_step_determinacy [lemma, in CoqIntro]
some_bool [constructor, in CoqIntro]
some_nat [constructor, in CoqIntro]
sort_dec [lemma, in ListFacts]
Sort_eq_head [lemma, in ListFacts]
Sort_InA_eq_ext [lemma, in ListFacts]
sort_unique [lemma, in ListFacts]
STLC_Solutions [library]
STLC_Tutorial [library]
strongly_diverges [definition, in CoqIntro]
sub [inductive, in Fsub_LetSum_Definitions]
sub [inductive, in Fsub_Definitions]
subst [definition, in STLC_Solutions]
subst [definition, in STLC_Tutorial]
subst_ee [definition, in Fsub_Infrastructure]
subst_ee [definition, in Fsub_LetSum_Infrastructure]
subst_ee_expr [lemma, in Fsub_LetSum_Infrastructure]
subst_ee_expr [lemma, in Fsub_Infrastructure]
subst_ee_fresh [lemma, in Fsub_Infrastructure]
subst_ee_fresh [lemma, in Fsub_LetSum_Infrastructure]
subst_ee_intro [lemma, in Fsub_Infrastructure]
subst_ee_intro [lemma, in Fsub_LetSum_Infrastructure]
subst_ee_intro_rec [lemma, in Fsub_Infrastructure]
subst_ee_intro_rec [lemma, in Fsub_LetSum_Infrastructure]
subst_ee_open_ee [lemma, in Fsub_Infrastructure]
subst_ee_open_ee [lemma, in Fsub_LetSum_Infrastructure]
subst_ee_open_ee_rec [lemma, in Fsub_LetSum_Infrastructure]
subst_ee_open_ee_rec [lemma, in Fsub_Infrastructure]
subst_ee_open_ee_var [lemma, in Fsub_Infrastructure]
subst_ee_open_ee_var [lemma, in Fsub_LetSum_Infrastructure]
subst_ee_open_te [lemma, in Fsub_Infrastructure]
subst_ee_open_te [lemma, in Fsub_LetSum_Infrastructure]
subst_ee_open_te_rec [lemma, in Fsub_Infrastructure]
subst_ee_open_te_rec [lemma, in Fsub_LetSum_Infrastructure]
subst_ee_open_te_var [lemma, in Fsub_LetSum_Infrastructure]
subst_ee_open_te_var [lemma, in Fsub_Infrastructure]
subst_fresh [lemma, in STLC_Tutorial]
subst_fresh [lemma, in STLC_Solutions]
subst_intro [lemma, in STLC_Solutions]
subst_intro [lemma, in STLC_Tutorial]
subst_lc [lemma, in STLC_Tutorial]
subst_lc [lemma, in STLC_Solutions]
subst_lc_alternate_proof [lemma, in STLC_Tutorial]
subst_lc_alternate_proof [lemma, in STLC_Solutions]
subst_lc_1 [lemma, in STLC_Solutions]
subst_lc_1 [lemma, in STLC_Tutorial]
subst_open_rec [lemma, in STLC_Tutorial]
subst_open_rec [lemma, in STLC_Solutions]
subst_open_var [lemma, in STLC_Solutions]
subst_open_var [lemma, in STLC_Tutorial]
subst_tb [definition, in Fsub_LetSum_Infrastructure]
subst_tb [definition, in Fsub_Infrastructure]
subst_te [definition, in Fsub_LetSum_Infrastructure]
subst_te [definition, in Fsub_Infrastructure]
subst_te_expr [lemma, in Fsub_Infrastructure]
subst_te_expr [lemma, in Fsub_LetSum_Infrastructure]
subst_te_fresh [lemma, in Fsub_Infrastructure]
subst_te_fresh [lemma, in Fsub_LetSum_Infrastructure]
subst_te_intro [lemma, in Fsub_Infrastructure]
subst_te_intro [lemma, in Fsub_LetSum_Infrastructure]
subst_te_intro_rec [lemma, in Fsub_Infrastructure]
subst_te_intro_rec [lemma, in Fsub_LetSum_Infrastructure]
subst_te_open_ee [lemma, in Fsub_LetSum_Infrastructure]
subst_te_open_ee [lemma, in Fsub_Infrastructure]
subst_te_open_ee_rec [lemma, in Fsub_Infrastructure]
subst_te_open_ee_rec [lemma, in Fsub_LetSum_Infrastructure]
subst_te_open_ee_var [lemma, in Fsub_LetSum_Infrastructure]
subst_te_open_ee_var [lemma, in Fsub_Infrastructure]
subst_te_open_te [lemma, in Fsub_LetSum_Infrastructure]
subst_te_open_te [lemma, in Fsub_Infrastructure]
subst_te_open_te_rec [lemma, in Fsub_Infrastructure]
subst_te_open_te_rec [lemma, in Fsub_LetSum_Infrastructure]
subst_te_open_te_var [lemma, in Fsub_LetSum_Infrastructure]
subst_te_open_te_var [lemma, in Fsub_Infrastructure]
subst_tt [definition, in Fsub_LetSum_Infrastructure]
subst_tt [definition, in Fsub_Infrastructure]
subst_tt_fresh [lemma, in Fsub_LetSum_Infrastructure]
subst_tt_fresh [lemma, in Fsub_Infrastructure]
subst_tt_intro [lemma, in Fsub_LetSum_Infrastructure]
subst_tt_intro [lemma, in Fsub_Infrastructure]
subst_tt_intro_rec [lemma, in Fsub_LetSum_Infrastructure]
subst_tt_intro_rec [lemma, in Fsub_Infrastructure]
subst_tt_open_tt [lemma, in Fsub_Infrastructure]
subst_tt_open_tt [lemma, in Fsub_LetSum_Infrastructure]
subst_tt_open_tt_rec [lemma, in Fsub_Infrastructure]
subst_tt_open_tt_rec [lemma, in Fsub_LetSum_Infrastructure]
subst_tt_open_tt_var [lemma, in Fsub_Infrastructure]
subst_tt_open_tt_var [lemma, in Fsub_LetSum_Infrastructure]
subst_tt_type [lemma, in Fsub_LetSum_Infrastructure]
subst_tt_type [lemma, in Fsub_Infrastructure]
sub_all [constructor, in Fsub_Definitions]
sub_all [constructor, in Fsub_LetSum_Definitions]
sub_arrow [constructor, in Fsub_LetSum_Definitions]
sub_arrow [constructor, in Fsub_Definitions]
sub_narrowing [lemma, in Fsub_LetSum_Soundness]
sub_narrowing [lemma, in Fsub_Soundness]
sub_narrowing_aux [lemma, in Fsub_LetSum_Soundness]
sub_narrowing_aux [lemma, in Fsub_Soundness]
sub_reflexivity [lemma, in Fsub_LetSum_Soundness]
sub_reflexivity [lemma, in Fsub_Soundness]
sub_refl_tvar [constructor, in Fsub_LetSum_Definitions]
sub_refl_tvar [constructor, in Fsub_Definitions]
sub_regular [lemma, in Fsub_Lemmas]
sub_regular [lemma, in Fsub_LetSum_Lemmas]
sub_strengthening [lemma, in Fsub_Soundness]
sub_strengthening [lemma, in Fsub_LetSum_Soundness]
sub_sum [constructor, in Fsub_LetSum_Definitions]
sub_through_subst_tt [lemma, in Fsub_Soundness]
sub_through_subst_tt [lemma, in Fsub_LetSum_Soundness]
sub_top [constructor, in Fsub_LetSum_Definitions]
sub_top [constructor, in Fsub_Definitions]
sub_transitivity [lemma, in Fsub_LetSum_Soundness]
sub_transitivity [lemma, in Fsub_Soundness]
sub_trans_tvar [constructor, in Fsub_LetSum_Definitions]
sub_trans_tvar [constructor, in Fsub_Definitions]
sub_weakening [lemma, in Fsub_Soundness]
sub_weakening [lemma, in Fsub_LetSum_Soundness]
succ_not_circular [lemma, in CoqIntro]
succ_not_circular_sol [lemma, in CoqIntro]
T
tm [inductive, in CoqIntro]tm_bool_tm [lemma, in CoqIntro]
tm_false [constructor, in CoqIntro]
tm_if [constructor, in CoqIntro]
tm_iszero [constructor, in CoqIntro]
tm_nat_tm [lemma, in CoqIntro]
tm_pred [constructor, in CoqIntro]
tm_succ [constructor, in CoqIntro]
tm_to_bool [definition, in CoqIntro]
tm_to_bool_dom_includes_bvalue [lemma, in CoqIntro]
tm_to_bool_dom_includes_bvalue_sol [lemma, in CoqIntro]
tm_to_bool_dom_only_bvalue [lemma, in CoqIntro]
tm_to_bool_dom_only_bvalue_sol [lemma, in CoqIntro]
tm_to_nat [definition, in CoqIntro]
tm_to_nat_dom_includes_nvalue [lemma, in CoqIntro]
tm_to_nat_dom_includes_nvalue_sol [lemma, in CoqIntro]
tm_to_nat_dom_only_nvalue [lemma, in CoqIntro]
tm_to_nat_dom_only_nvalue_sol [lemma, in CoqIntro]
tm_true [constructor, in CoqIntro]
tm_zero [constructor, in CoqIntro]
transitivity_on [definition, in Fsub_LetSum_Soundness]
transitivity_on [definition, in Fsub_Soundness]
true_and_succ_zero_values [lemma, in CoqIntro]
two [definition, in STLC_Solutions]
two_values [lemma, in CoqIntro]
two_values_sol [lemma, in CoqIntro]
typ [inductive, in Fsub_LetSum_Definitions]
typ [inductive, in Fsub_Definitions]
typ [inductive, in STLC_Solutions]
typ [inductive, in STLC_Tutorial]
type [inductive, in Fsub_Definitions]
type [inductive, in Fsub_LetSum_Definitions]
type_all [constructor, in Fsub_LetSum_Definitions]
type_all [constructor, in Fsub_Definitions]
type_arrow [constructor, in Fsub_LetSum_Definitions]
type_arrow [constructor, in Fsub_Definitions]
type_from_wf_typ [lemma, in Fsub_Lemmas]
type_from_wf_typ [lemma, in Fsub_LetSum_Lemmas]
type_sum [constructor, in Fsub_LetSum_Definitions]
type_top [constructor, in Fsub_LetSum_Definitions]
type_top [constructor, in Fsub_Definitions]
type_var [constructor, in Fsub_LetSum_Definitions]
type_var [constructor, in Fsub_Definitions]
typing [inductive, in STLC_Solutions]
typing [inductive, in Fsub_Definitions]
typing [inductive, in Fsub_LetSum_Definitions]
typing [inductive, in STLC_Tutorial]
typing_abs [constructor, in STLC_Solutions]
typing_abs [constructor, in Fsub_Definitions]
typing_abs [constructor, in Fsub_LetSum_Definitions]
typing_abs [constructor, in STLC_Tutorial]
typing_app [constructor, in STLC_Solutions]
typing_app [constructor, in Fsub_Definitions]
typing_app [constructor, in STLC_Tutorial]
typing_app [constructor, in Fsub_LetSum_Definitions]
typing_case [constructor, in Fsub_LetSum_Definitions]
typing_inl [constructor, in Fsub_LetSum_Definitions]
typing_inr [constructor, in Fsub_LetSum_Definitions]
typing_inv_abs [lemma, in Fsub_Soundness]
typing_inv_abs [lemma, in Fsub_LetSum_Soundness]
typing_inv_inl [lemma, in Fsub_LetSum_Soundness]
typing_inv_inr [lemma, in Fsub_LetSum_Soundness]
typing_inv_tabs [lemma, in Fsub_LetSum_Soundness]
typing_inv_tabs [lemma, in Fsub_Soundness]
typing_let [constructor, in Fsub_LetSum_Definitions]
typing_narrowing [lemma, in Fsub_LetSum_Soundness]
typing_narrowing [lemma, in Fsub_Soundness]
typing_regular [lemma, in Fsub_LetSum_Lemmas]
typing_regular [lemma, in Fsub_Lemmas]
typing_regular_lc [lemma, in STLC_Solutions]
typing_regular_lc [lemma, in STLC_Tutorial]
typing_regular_ok [lemma, in STLC_Tutorial]
typing_regular_ok [lemma, in STLC_Solutions]
typing_sub [constructor, in Fsub_Definitions]
typing_sub [constructor, in Fsub_LetSum_Definitions]
typing_subst [lemma, in STLC_Solutions]
typing_subst [lemma, in STLC_Tutorial]
typing_subst_strengthened [lemma, in STLC_Solutions]
typing_subst_strengthened [lemma, in STLC_Tutorial]
typing_subst_var_case [lemma, in STLC_Solutions]
typing_subst_var_case [lemma, in STLC_Tutorial]
typing_tabs [constructor, in Fsub_Definitions]
typing_tabs [constructor, in Fsub_LetSum_Definitions]
typing_tapp [constructor, in Fsub_Definitions]
typing_tapp [constructor, in Fsub_LetSum_Definitions]
typing_through_subst_ee [lemma, in Fsub_LetSum_Soundness]
typing_through_subst_ee [lemma, in Fsub_Soundness]
typing_through_subst_te [lemma, in Fsub_Soundness]
typing_through_subst_te [lemma, in Fsub_LetSum_Soundness]
typing_var [constructor, in STLC_Tutorial]
typing_var [constructor, in Fsub_LetSum_Definitions]
typing_var [constructor, in Fsub_Definitions]
typing_var [constructor, in STLC_Solutions]
typing_weakening [lemma, in Fsub_Soundness]
typing_weakening [lemma, in STLC_Solutions]
typing_weakening [lemma, in Fsub_LetSum_Soundness]
typing_weakening [lemma, in STLC_Tutorial]
typing_weakening_strengthened [lemma, in STLC_Tutorial]
typing_weakening_strengthened [lemma, in STLC_Solutions]
typing_weakening_strengthened_0 [lemma, in STLC_Solutions]
typing_weakening_strengthened_0 [lemma, in STLC_Tutorial]
typing_weakening_0 [lemma, in STLC_Solutions]
typing_weakening_0 [lemma, in STLC_Tutorial]
typ_all [constructor, in Fsub_LetSum_Definitions]
typ_all [constructor, in Fsub_Definitions]
typ_arrow [constructor, in Fsub_LetSum_Definitions]
typ_arrow [constructor, in Fsub_Definitions]
typ_arrow [constructor, in STLC_Tutorial]
typ_arrow [constructor, in STLC_Solutions]
typ_base [constructor, in STLC_Tutorial]
typ_base [constructor, in STLC_Solutions]
typ_bvar [constructor, in Fsub_LetSum_Definitions]
typ_bvar [constructor, in Fsub_Definitions]
typ_fvar [constructor, in Fsub_LetSum_Definitions]
typ_fvar [constructor, in Fsub_Definitions]
typ_sum [constructor, in Fsub_LetSum_Definitions]
typ_top [constructor, in Fsub_LetSum_Definitions]
typ_top [constructor, in Fsub_Definitions]
U
unfold_example [lemma, in CoqIntro]V
value [definition, in CoqIntro]value [inductive, in Fsub_LetSum_Definitions]
value [inductive, in STLC_Tutorial]
value [inductive, in Fsub_Definitions]
value [inductive, in STLC_Solutions]
value_abs [constructor, in Fsub_LetSum_Definitions]
value_abs [constructor, in Fsub_Definitions]
value_abs [constructor, in STLC_Tutorial]
value_abs [constructor, in STLC_Solutions]
value_can_expand [lemma, in CoqIntro]
value_can_expand_sol [lemma, in CoqIntro]
value_inl [constructor, in Fsub_LetSum_Definitions]
value_inr [constructor, in Fsub_LetSum_Definitions]
value_is_normal_form [lemma, in CoqIntro]
value_is_normal_form_sol [lemma, in CoqIntro]
value_regular [lemma, in STLC_Tutorial]
value_regular [lemma, in Fsub_LetSum_Lemmas]
value_regular [lemma, in Fsub_Lemmas]
value_regular [lemma, in STLC_Solutions]
value_succ_nvalue [lemma, in CoqIntro]
value_tabs [constructor, in Fsub_LetSum_Definitions]
value_tabs [constructor, in Fsub_Definitions]
W
wf_env [inductive, in Fsub_Definitions]wf_env [inductive, in Fsub_LetSum_Definitions]
wf_env_empty [constructor, in Fsub_LetSum_Definitions]
wf_env_empty [constructor, in Fsub_Definitions]
wf_env_narrowing [lemma, in Fsub_LetSum_Lemmas]
wf_env_narrowing [lemma, in Fsub_Lemmas]
wf_env_strengthening [lemma, in Fsub_LetSum_Lemmas]
wf_env_strengthening [lemma, in Fsub_Lemmas]
wf_env_sub [constructor, in Fsub_Definitions]
wf_env_sub [constructor, in Fsub_LetSum_Definitions]
wf_env_subst_tb [lemma, in Fsub_LetSum_Lemmas]
wf_env_subst_tb [lemma, in Fsub_Lemmas]
wf_env_typ [constructor, in Fsub_LetSum_Definitions]
wf_env_typ [constructor, in Fsub_Definitions]
wf_typ [inductive, in Fsub_LetSum_Definitions]
wf_typ [inductive, in Fsub_Definitions]
wf_typ_all [constructor, in Fsub_Definitions]
wf_typ_all [constructor, in Fsub_LetSum_Definitions]
wf_typ_arrow [constructor, in Fsub_Definitions]
wf_typ_arrow [constructor, in Fsub_LetSum_Definitions]
wf_typ_from_binds_typ [lemma, in Fsub_Lemmas]
wf_typ_from_binds_typ [lemma, in Fsub_LetSum_Lemmas]
wf_typ_from_wf_env_sub [lemma, in Fsub_Lemmas]
wf_typ_from_wf_env_sub [lemma, in Fsub_LetSum_Lemmas]
wf_typ_from_wf_env_typ [lemma, in Fsub_LetSum_Lemmas]
wf_typ_from_wf_env_typ [lemma, in Fsub_Lemmas]
wf_typ_narrowing [lemma, in Fsub_LetSum_Lemmas]
wf_typ_narrowing [lemma, in Fsub_Lemmas]
wf_typ_open [lemma, in Fsub_Lemmas]
wf_typ_open [lemma, in Fsub_LetSum_Lemmas]
wf_typ_strengthening [lemma, in Fsub_LetSum_Lemmas]
wf_typ_strengthening [lemma, in Fsub_Lemmas]
wf_typ_subst_tb [lemma, in Fsub_Lemmas]
wf_typ_subst_tb [lemma, in Fsub_LetSum_Lemmas]
wf_typ_sum [constructor, in Fsub_LetSum_Definitions]
wf_typ_top [constructor, in Fsub_Definitions]
wf_typ_top [constructor, in Fsub_LetSum_Definitions]
wf_typ_var [constructor, in Fsub_Definitions]
wf_typ_var [constructor, in Fsub_LetSum_Definitions]
wf_typ_weakening [lemma, in Fsub_LetSum_Lemmas]
wf_typ_weakening [lemma, in Fsub_Lemmas]
wf_typ_weaken_head [lemma, in Fsub_Lemmas]
wf_typ_weaken_head [lemma, in Fsub_LetSum_Lemmas]
Y
Y [axiom, in STLC_Tutorial]Y [axiom, in STLC_Solutions]
Z
Z [axiom, in STLC_Tutorial]Z [axiom, in STLC_Solutions]
Axiom Index
A
atom [in Atom]atom_fresh_for_list [in Atom]
E
eq_atom_dec [in Atom]eq_if_Equal [in FiniteSets]
Y
Y [in STLC_Tutorial]Y [in STLC_Solutions]
Z
Z [in STLC_Tutorial]Z [in STLC_Solutions]
Lemma Index
A
ATOM.Atom_as_OT.AtomSet.atom_fresh_for_set [in Atom]ATOM.Atom_as_OT.AtomSet.example_pick_fresh_use [in Atom]
auto_example [in CoqIntro]
B
binds_concat_inv [in Environment]binds_concat_ok [in Environment]
binds_fresh [in Environment]
binds_head [in Environment]
binds_In [in Environment]
binds_map [in Environment]
binds_mid [in Environment]
binds_mid_eq [in Environment]
binds_mid_eq_cons [in Environment]
binds_remove_mid [in Environment]
binds_remove_mid_cons [in Environment]
binds_singleton [in Environment]
binds_singleton_inv [in Environment]
binds_tail [in Environment]
binds_weaken [in Environment]
binds_weaken_at_head [in Environment]
body_from_expr_let [in Fsub_LetSum_Infrastructure]
body_inl_from_expr_case [in Fsub_LetSum_Infrastructure]
body_inr_from_expr_case [in Fsub_LetSum_Infrastructure]
bool_tm_bool [in CoqIntro]
C
canonical_form_abs [in Fsub_Soundness]canonical_form_abs [in Fsub_LetSum_Soundness]
canonical_form_sum [in Fsub_LetSum_Soundness]
canonical_form_tabs [in Fsub_LetSum_Soundness]
canonical_form_tabs [in Fsub_Soundness]
concat_assoc [in Environment]
concat_nil [in Environment]
cons_concat [in Environment]
cons_concat_assoc [in Environment]
contradictory_equalities_exercise [in CoqIntro]
contradictory_equalities_exercise_sol [in CoqIntro]
D
Decide.FSetDecideAuxiliary.dec_eq [in FSetDecide]Decide.FSetDecideAuxiliary.dec_In [in FSetDecide]
Decide.FSetDecideTestCases.eq_chain_test [in FSetDecide]
Decide.FSetDecideTestCases.function_test_1 [in FSetDecide]
Decide.FSetDecideTestCases.function_test_2 [in FSetDecide]
Decide.FSetDecideTestCases.test_eq_disjunction [in FSetDecide]
Decide.FSetDecideTestCases.test_eq_neq_trans_1 [in FSetDecide]
Decide.FSetDecideTestCases.test_eq_neq_trans_2 [in FSetDecide]
Decide.FSetDecideTestCases.test_eq_trans_1 [in FSetDecide]
Decide.FSetDecideTestCases.test_eq_trans_2 [in FSetDecide]
Decide.FSetDecideTestCases.test_iff_conj [in FSetDecide]
Decide.FSetDecideTestCases.test_In_singleton [in FSetDecide]
Decide.FSetDecideTestCases.test_not_In_conj [in FSetDecide]
Decide.FSetDecideTestCases.test_not_In_disj [in FSetDecide]
Decide.FSetDecideTestCases.test_set_ops_1 [in FSetDecide]
Decide.FSetDecideTestCases.test_Subset_add_remove [in FSetDecide]
Decide.FSetDecideTestCases.test_too_complex [in FSetDecide]
Decide.FSetLogicalFacts.contrapositive [in FSetDecide]
Decide.FSetLogicalFacts.dec_iff [in FSetDecide]
Decide.FSetLogicalFacts.imp_not_l [in FSetDecide]
Decide.FSetLogicalFacts.not_and_iff [in FSetDecide]
Decide.FSetLogicalFacts.not_false_iff [in FSetDecide]
Decide.FSetLogicalFacts.not_imp_iff [in FSetDecide]
Decide.FSetLogicalFacts.not_imp_rev_iff [in FSetDecide]
Decide.FSetLogicalFacts.not_not_iff [in FSetDecide]
Decide.FSetLogicalFacts.not_or_iff [in FSetDecide]
Decide.FSetLogicalFacts.not_true_iff [in FSetDecide]
Decide.FSetLogicalFacts.or_not_l_iff_1 [in FSetDecide]
Decide.FSetLogicalFacts.or_not_l_iff_2 [in FSetDecide]
Decide.FSetLogicalFacts.or_not_r_iff_1 [in FSetDecide]
Decide.FSetLogicalFacts.or_not_r_iff_2 [in FSetDecide]
Decide.FSetLogicalFacts.test_pull [in FSetDecide]
Decide.FSetLogicalFacts.test_push [in FSetDecide]
demo_open [in STLC_Tutorial]
demo_open [in STLC_Solutions]
demo_subst1 [in STLC_Solutions]
demo_subst1 [in STLC_Tutorial]
destruct_example [in CoqIntro]
destruct_negation_example [in CoqIntro]
dom_concat [in Environment]
dom_map [in Environment]
dom_nil [in Environment]
dom_push [in Environment]
dom_single [in Environment]
dom_singleton_list [in Environment]
E
eauto_example [in CoqIntro]eauto_using_example [in CoqIntro]
elim_incl_app [in ListFacts]
elim_incl_cons [in ListFacts]
elim_not_In_app [in ListFacts]
elim_not_In_cons [in ListFacts]
equality_example_1 [in CoqIntro]
equality_example_2a [in CoqIntro]
equality_example_2b [in CoqIntro]
equality_example_2c [in CoqIntro]
equality_example_3 [in CoqIntro]
equality_example_4 [in CoqIntro]
equality_exercise [in CoqIntro]
equality_exercise_sol [in CoqIntro]
eq_rect_eq_list [in ListFacts]
eval_deterministic [in CoqIntro]
eval_deterministic_sol [in CoqIntro]
eval_fact_exercise [in CoqIntro]
eval_fact_exercise_sol [in CoqIntro]
eval_full_eval_sol [in CoqIntro]
eval_many_rtc_sol [in CoqIntro]
eval_regular [in STLC_Tutorial]
eval_regular [in STLC_Solutions]
eval_rtc_many_sol [in CoqIntro]
exists_iszero_nvalue [in CoqIntro]
exists_iszero_nvalue_sol [in CoqIntro]
exists_pred_zero [in CoqIntro]
expr_case_from_body [in Fsub_LetSum_Infrastructure]
expr_let_from_body [in Fsub_LetSum_Infrastructure]
e_if_true_or_false [in CoqIntro]
e_iszero_nvalue [in CoqIntro]
e_succ_pred_succ [in CoqIntro]
F
False_hypothesis [in CoqIntro]fresh_mid_head [in Environment]
fresh_mid_tail [in Environment]
full_eval_complete_sol [in CoqIntro]
full_eval_from_value_sol [in CoqIntro]
full_eval_to_value_sol [in CoqIntro]
I
if_bvalue [in CoqIntro]InA_iff_In [in ListFacts]
incl_nil [in ListFacts]
incl_trans [in ListFacts]
interp_fully_reduces_sol [in CoqIntro]
interp_reduces_sol [in CoqIntro]
inversion_exercise [in CoqIntro]
inversion_exercise_sol [in CoqIntro]
In_incl [in ListFacts]
L
lelistA_dec [in ListFacts]lelistA_unique [in ListFacts]
M
map_concat [in Environment]map_nil [in Environment]
map_push [in Environment]
map_single [in Environment]
map_singleton_list [in Environment]
map_subst_tb_id [in Fsub_Lemmas]
map_subst_tb_id [in Fsub_LetSum_Lemmas]
m_if [in CoqIntro]
m_iftrue_step [in CoqIntro]
m_iftrue_step_sol [in CoqIntro]
m_if_iszero_conj [in CoqIntro]
m_if_iszero_conj_sol [in CoqIntro]
m_iszero [in CoqIntro]
m_iszero_nvalue [in CoqIntro]
m_one [in CoqIntro]
m_one_sol [in CoqIntro]
m_pred [in CoqIntro]
m_pred_sol [in CoqIntro]
m_succ [in CoqIntro]
m_succ_pred_succ [in CoqIntro]
m_succ_pred_succ_alt [in CoqIntro]
m_succ_sol [in CoqIntro]
m_three [in CoqIntro]
m_three_conj [in CoqIntro]
m_trans [in CoqIntro]
m_trans_sol [in CoqIntro]
m_two [in CoqIntro]
m_two_conj [in CoqIntro]
m_two_exists [in CoqIntro]
m_two_exists' [in CoqIntro]
m_two_exists'' [in CoqIntro]
m_two_sol [in CoqIntro]
N
nat_tm_nat [in CoqIntro]negation_exercise [in CoqIntro]
negation_exercise_sol [in CoqIntro]
nil_concat [in Environment]
normal_form_from_forall [in CoqIntro]
normal_form_from_forall_sol [in CoqIntro]
normal_form_if [in CoqIntro]
normal_form_if_sol [in CoqIntro]
normal_form_succ [in CoqIntro]
normal_form_to_forall [in CoqIntro]
normal_form_to_forall_sol [in CoqIntro]
Notin.elim_notin_singleton [in FSetNotin]
Notin.elim_notin_singleton' [in FSetNotin]
Notin.elim_notin_union [in FSetNotin]
Notin.in_singleton [in FSetNotin]
Notin.notin_empty [in FSetNotin]
Notin.notin_singleton [in FSetNotin]
Notin.notin_singleton_rw [in FSetNotin]
Notin.notin_singleton_swap [in FSetNotin]
Notin.notin_union [in FSetNotin]
Notin.test_notin_solve_1 [in FSetNotin]
Notin.test_notin_solve_2 [in FSetNotin]
Notin.test_notin_solve_3 [in FSetNotin]
Notin.test_notin_solve_4 [in FSetNotin]
Notin.test_notin_solve_5 [in FSetNotin]
notin_fv_tt_open [in Fsub_LetSum_Lemmas]
notin_fv_tt_open [in Fsub_Lemmas]
notin_fv_wf [in Fsub_LetSum_Lemmas]
notin_fv_wf [in Fsub_Lemmas]
not_InA_if_Sort_Inf [in ListFacts]
not_In_app [in ListFacts]
not_in_cons [in ListFacts]
nvalue_is_normal_form [in CoqIntro]
nvalue_is_normal_form' [in CoqIntro]
O
ok_from_wf_env [in Fsub_Lemmas]ok_from_wf_env [in Fsub_LetSum_Lemmas]
ok_map [in Environment]
ok_map_app_l [in Environment]
ok_push [in Environment]
ok_remove_mid [in Environment]
ok_remove_mid_cons [in Environment]
ok_singleton [in Environment]
open_abs [in STLC_Solutions]
open_abs [in STLC_Tutorial]
open_ee_body_e [in Fsub_LetSum_Infrastructure]
open_ee_rec_expr [in Fsub_Infrastructure]
open_ee_rec_expr [in Fsub_LetSum_Infrastructure]
open_ee_rec_expr_aux [in Fsub_Infrastructure]
open_ee_rec_expr_aux [in Fsub_LetSum_Infrastructure]
open_ee_rec_type_aux [in Fsub_Infrastructure]
open_ee_rec_type_aux [in Fsub_LetSum_Infrastructure]
open_rec_lc [in STLC_Tutorial]
open_rec_lc [in STLC_Solutions]
open_rec_lc_core [in STLC_Tutorial]
open_rec_lc_core [in STLC_Solutions]
open_rec_lc_0 [in STLC_Solutions]
open_rec_lc_0 [in STLC_Tutorial]
open_rec_lc_1 [in STLC_Tutorial]
open_rec_lc_1 [in STLC_Solutions]
open_te_rec_expr [in Fsub_Infrastructure]
open_te_rec_expr [in Fsub_LetSum_Infrastructure]
open_te_rec_expr_aux [in Fsub_LetSum_Infrastructure]
open_te_rec_expr_aux [in Fsub_Infrastructure]
open_te_rec_type_aux [in Fsub_LetSum_Infrastructure]
open_te_rec_type_aux [in Fsub_Infrastructure]
open_tt_rec_type [in Fsub_Infrastructure]
open_tt_rec_type [in Fsub_LetSum_Infrastructure]
open_tt_rec_type_aux [in Fsub_Infrastructure]
open_tt_rec_type_aux [in Fsub_LetSum_Infrastructure]
P
pred_not_circular [in CoqIntro]pred_not_circular_sol [in CoqIntro]
preservation [in Fsub_Soundness]
preservation [in STLC_Tutorial]
preservation [in Fsub_LetSum_Soundness]
preservation [in STLC_Solutions]
progress [in STLC_Solutions]
progress [in Fsub_Soundness]
progress [in STLC_Tutorial]
progress [in Fsub_LetSum_Soundness]
R
red_regular [in Fsub_LetSum_Lemmas]red_regular [in Fsub_Lemmas]
remember_example [in CoqIntro]
S
single_step_to_multi_step_determinacy [in CoqIntro]sort_dec [in ListFacts]
Sort_eq_head [in ListFacts]
Sort_InA_eq_ext [in ListFacts]
sort_unique [in ListFacts]
subst_ee_expr [in Fsub_LetSum_Infrastructure]
subst_ee_expr [in Fsub_Infrastructure]
subst_ee_fresh [in Fsub_Infrastructure]
subst_ee_fresh [in Fsub_LetSum_Infrastructure]
subst_ee_intro [in Fsub_Infrastructure]
subst_ee_intro [in Fsub_LetSum_Infrastructure]
subst_ee_intro_rec [in Fsub_Infrastructure]
subst_ee_intro_rec [in Fsub_LetSum_Infrastructure]
subst_ee_open_ee [in Fsub_Infrastructure]
subst_ee_open_ee [in Fsub_LetSum_Infrastructure]
subst_ee_open_ee_rec [in Fsub_LetSum_Infrastructure]
subst_ee_open_ee_rec [in Fsub_Infrastructure]
subst_ee_open_ee_var [in Fsub_Infrastructure]
subst_ee_open_ee_var [in Fsub_LetSum_Infrastructure]
subst_ee_open_te [in Fsub_Infrastructure]
subst_ee_open_te [in Fsub_LetSum_Infrastructure]
subst_ee_open_te_rec [in Fsub_Infrastructure]
subst_ee_open_te_rec [in Fsub_LetSum_Infrastructure]
subst_ee_open_te_var [in Fsub_LetSum_Infrastructure]
subst_ee_open_te_var [in Fsub_Infrastructure]
subst_fresh [in STLC_Tutorial]
subst_fresh [in STLC_Solutions]
subst_intro [in STLC_Solutions]
subst_intro [in STLC_Tutorial]
subst_lc [in STLC_Tutorial]
subst_lc [in STLC_Solutions]
subst_lc_alternate_proof [in STLC_Tutorial]
subst_lc_alternate_proof [in STLC_Solutions]
subst_lc_1 [in STLC_Solutions]
subst_lc_1 [in STLC_Tutorial]
subst_open_rec [in STLC_Tutorial]
subst_open_rec [in STLC_Solutions]
subst_open_var [in STLC_Solutions]
subst_open_var [in STLC_Tutorial]
subst_te_expr [in Fsub_Infrastructure]
subst_te_expr [in Fsub_LetSum_Infrastructure]
subst_te_fresh [in Fsub_Infrastructure]
subst_te_fresh [in Fsub_LetSum_Infrastructure]
subst_te_intro [in Fsub_Infrastructure]
subst_te_intro [in Fsub_LetSum_Infrastructure]
subst_te_intro_rec [in Fsub_Infrastructure]
subst_te_intro_rec [in Fsub_LetSum_Infrastructure]
subst_te_open_ee [in Fsub_LetSum_Infrastructure]
subst_te_open_ee [in Fsub_Infrastructure]
subst_te_open_ee_rec [in Fsub_Infrastructure]
subst_te_open_ee_rec [in Fsub_LetSum_Infrastructure]
subst_te_open_ee_var [in Fsub_LetSum_Infrastructure]
subst_te_open_ee_var [in Fsub_Infrastructure]
subst_te_open_te [in Fsub_LetSum_Infrastructure]
subst_te_open_te [in Fsub_Infrastructure]
subst_te_open_te_rec [in Fsub_Infrastructure]
subst_te_open_te_rec [in Fsub_LetSum_Infrastructure]
subst_te_open_te_var [in Fsub_LetSum_Infrastructure]
subst_te_open_te_var [in Fsub_Infrastructure]
subst_tt_fresh [in Fsub_LetSum_Infrastructure]
subst_tt_fresh [in Fsub_Infrastructure]
subst_tt_intro [in Fsub_LetSum_Infrastructure]
subst_tt_intro [in Fsub_Infrastructure]
subst_tt_intro_rec [in Fsub_LetSum_Infrastructure]
subst_tt_intro_rec [in Fsub_Infrastructure]
subst_tt_open_tt [in Fsub_Infrastructure]
subst_tt_open_tt [in Fsub_LetSum_Infrastructure]
subst_tt_open_tt_rec [in Fsub_Infrastructure]
subst_tt_open_tt_rec [in Fsub_LetSum_Infrastructure]
subst_tt_open_tt_var [in Fsub_Infrastructure]
subst_tt_open_tt_var [in Fsub_LetSum_Infrastructure]
subst_tt_type [in Fsub_LetSum_Infrastructure]
subst_tt_type [in Fsub_Infrastructure]
sub_narrowing [in Fsub_LetSum_Soundness]
sub_narrowing [in Fsub_Soundness]
sub_narrowing_aux [in Fsub_LetSum_Soundness]
sub_narrowing_aux [in Fsub_Soundness]
sub_reflexivity [in Fsub_LetSum_Soundness]
sub_reflexivity [in Fsub_Soundness]
sub_regular [in Fsub_Lemmas]
sub_regular [in Fsub_LetSum_Lemmas]
sub_strengthening [in Fsub_Soundness]
sub_strengthening [in Fsub_LetSum_Soundness]
sub_through_subst_tt [in Fsub_Soundness]
sub_through_subst_tt [in Fsub_LetSum_Soundness]
sub_transitivity [in Fsub_LetSum_Soundness]
sub_transitivity [in Fsub_Soundness]
sub_weakening [in Fsub_Soundness]
sub_weakening [in Fsub_LetSum_Soundness]
succ_not_circular [in CoqIntro]
succ_not_circular_sol [in CoqIntro]
T
tm_bool_tm [in CoqIntro]tm_nat_tm [in CoqIntro]
tm_to_bool_dom_includes_bvalue [in CoqIntro]
tm_to_bool_dom_includes_bvalue_sol [in CoqIntro]
tm_to_bool_dom_only_bvalue [in CoqIntro]
tm_to_bool_dom_only_bvalue_sol [in CoqIntro]
tm_to_nat_dom_includes_nvalue [in CoqIntro]
tm_to_nat_dom_includes_nvalue_sol [in CoqIntro]
tm_to_nat_dom_only_nvalue [in CoqIntro]
tm_to_nat_dom_only_nvalue_sol [in CoqIntro]
true_and_succ_zero_values [in CoqIntro]
two_values [in CoqIntro]
two_values_sol [in CoqIntro]
type_from_wf_typ [in Fsub_Lemmas]
type_from_wf_typ [in Fsub_LetSum_Lemmas]
typing_inv_abs [in Fsub_Soundness]
typing_inv_abs [in Fsub_LetSum_Soundness]
typing_inv_inl [in Fsub_LetSum_Soundness]
typing_inv_inr [in Fsub_LetSum_Soundness]
typing_inv_tabs [in Fsub_LetSum_Soundness]
typing_inv_tabs [in Fsub_Soundness]
typing_narrowing [in Fsub_LetSum_Soundness]
typing_narrowing [in Fsub_Soundness]
typing_regular [in Fsub_LetSum_Lemmas]
typing_regular [in Fsub_Lemmas]
typing_regular_lc [in STLC_Solutions]
typing_regular_lc [in STLC_Tutorial]
typing_regular_ok [in STLC_Tutorial]
typing_regular_ok [in STLC_Solutions]
typing_subst [in STLC_Solutions]
typing_subst [in STLC_Tutorial]
typing_subst_strengthened [in STLC_Solutions]
typing_subst_strengthened [in STLC_Tutorial]
typing_subst_var_case [in STLC_Solutions]
typing_subst_var_case [in STLC_Tutorial]
typing_through_subst_ee [in Fsub_LetSum_Soundness]
typing_through_subst_ee [in Fsub_Soundness]
typing_through_subst_te [in Fsub_Soundness]
typing_through_subst_te [in Fsub_LetSum_Soundness]
typing_weakening [in Fsub_Soundness]
typing_weakening [in STLC_Solutions]
typing_weakening [in Fsub_LetSum_Soundness]
typing_weakening [in STLC_Tutorial]
typing_weakening_strengthened [in STLC_Tutorial]
typing_weakening_strengthened [in STLC_Solutions]
typing_weakening_strengthened_0 [in STLC_Solutions]
typing_weakening_strengthened_0 [in STLC_Tutorial]
typing_weakening_0 [in STLC_Solutions]
typing_weakening_0 [in STLC_Tutorial]
U
unfold_example [in CoqIntro]V
value_can_expand [in CoqIntro]value_can_expand_sol [in CoqIntro]
value_is_normal_form [in CoqIntro]
value_is_normal_form_sol [in CoqIntro]
value_regular [in STLC_Tutorial]
value_regular [in Fsub_LetSum_Lemmas]
value_regular [in Fsub_Lemmas]
value_regular [in STLC_Solutions]
value_succ_nvalue [in CoqIntro]
W
wf_env_narrowing [in Fsub_LetSum_Lemmas]wf_env_narrowing [in Fsub_Lemmas]
wf_env_strengthening [in Fsub_LetSum_Lemmas]
wf_env_strengthening [in Fsub_Lemmas]
wf_env_subst_tb [in Fsub_LetSum_Lemmas]
wf_env_subst_tb [in Fsub_Lemmas]
wf_typ_from_binds_typ [in Fsub_Lemmas]
wf_typ_from_binds_typ [in Fsub_LetSum_Lemmas]
wf_typ_from_wf_env_sub [in Fsub_Lemmas]
wf_typ_from_wf_env_sub [in Fsub_LetSum_Lemmas]
wf_typ_from_wf_env_typ [in Fsub_LetSum_Lemmas]
wf_typ_from_wf_env_typ [in Fsub_Lemmas]
wf_typ_narrowing [in Fsub_LetSum_Lemmas]
wf_typ_narrowing [in Fsub_Lemmas]
wf_typ_open [in Fsub_Lemmas]
wf_typ_open [in Fsub_LetSum_Lemmas]
wf_typ_strengthening [in Fsub_LetSum_Lemmas]
wf_typ_strengthening [in Fsub_Lemmas]
wf_typ_subst_tb [in Fsub_Lemmas]
wf_typ_subst_tb [in Fsub_LetSum_Lemmas]
wf_typ_weakening [in Fsub_LetSum_Lemmas]
wf_typ_weakening [in Fsub_Lemmas]
wf_typ_weaken_head [in Fsub_Lemmas]
wf_typ_weaken_head [in Fsub_LetSum_Lemmas]
Constructor Index
A
abs [in STLC_Solutions]abs [in STLC_Tutorial]
app [in STLC_Solutions]
app [in STLC_Tutorial]
B
bind_sub [in Fsub_LetSum_Definitions]bind_sub [in Fsub_Definitions]
bind_typ [in Fsub_Definitions]
bind_typ [in Fsub_LetSum_Definitions]
bvar [in STLC_Tutorial]
bvar [in STLC_Solutions]
b_false [in CoqIntro]
b_true [in CoqIntro]
D
Decide.FSetDecideAuxiliary.elt_FSet_Prop [in FSetDecide]Decide.FSetDecideAuxiliary.Empty_FSet_Prop [in FSetDecide]
Decide.FSetDecideAuxiliary.Equal_FSet_Prop [in FSetDecide]
Decide.FSetDecideAuxiliary.eq_elt_prop [in FSetDecide]
Decide.FSetDecideAuxiliary.eq_Prop [in FSetDecide]
Decide.FSetDecideAuxiliary.Subset_FSet_Prop [in FSetDecide]
E
eval_app_1 [in STLC_Tutorial]eval_app_1 [in STLC_Solutions]
eval_app_2 [in STLC_Solutions]
eval_app_2 [in STLC_Tutorial]
eval_beta [in STLC_Solutions]
eval_beta [in STLC_Tutorial]
expr_abs [in Fsub_LetSum_Definitions]
expr_abs [in Fsub_Definitions]
expr_app [in Fsub_LetSum_Definitions]
expr_app [in Fsub_Definitions]
expr_case [in Fsub_LetSum_Definitions]
expr_inl [in Fsub_LetSum_Definitions]
expr_inr [in Fsub_LetSum_Definitions]
expr_let [in Fsub_LetSum_Definitions]
expr_tabs [in Fsub_LetSum_Definitions]
expr_tabs [in Fsub_Definitions]
expr_tapp [in Fsub_LetSum_Definitions]
expr_tapp [in Fsub_Definitions]
expr_var [in Fsub_Definitions]
expr_var [in Fsub_LetSum_Definitions]
exp_abs [in Fsub_Definitions]
exp_abs [in Fsub_LetSum_Definitions]
exp_app [in Fsub_Definitions]
exp_app [in Fsub_LetSum_Definitions]
exp_bvar [in Fsub_LetSum_Definitions]
exp_bvar [in Fsub_Definitions]
exp_case [in Fsub_LetSum_Definitions]
exp_fvar [in Fsub_LetSum_Definitions]
exp_fvar [in Fsub_Definitions]
exp_inl [in Fsub_LetSum_Definitions]
exp_inr [in Fsub_LetSum_Definitions]
exp_let [in Fsub_LetSum_Definitions]
exp_tabs [in Fsub_Definitions]
exp_tabs [in Fsub_LetSum_Definitions]
exp_tapp [in Fsub_LetSum_Definitions]
exp_tapp [in Fsub_Definitions]
e_if [in CoqIntro]
e_iffalse [in CoqIntro]
e_iftrue [in CoqIntro]
e_iszero [in CoqIntro]
e_iszerosucc [in CoqIntro]
e_iszerozero [in CoqIntro]
e_pred [in CoqIntro]
e_predsucc [in CoqIntro]
e_predzero [in CoqIntro]
e_succ [in CoqIntro]
F
fvar [in STLC_Tutorial]fvar [in STLC_Solutions]
f_iffalse [in CoqIntro]
f_iftrue [in CoqIntro]
f_iszerosucc [in CoqIntro]
f_iszerozero [in CoqIntro]
f_predsucc [in CoqIntro]
f_predzero [in CoqIntro]
f_succ [in CoqIntro]
f_value [in CoqIntro]
L
lc_abs [in STLC_Solutions]lc_abs [in STLC_Tutorial]
lc_app [in STLC_Tutorial]
lc_app [in STLC_Solutions]
lc_var [in STLC_Solutions]
lc_var [in STLC_Tutorial]
M
m_refl [in CoqIntro]m_step [in CoqIntro]
N
no_bool [in CoqIntro]no_nat [in CoqIntro]
n_succ [in CoqIntro]
n_zero [in CoqIntro]
O
ok_cons [in Environment]ok_nil [in Environment]
R
red_abs [in Fsub_LetSum_Definitions]red_abs [in Fsub_Definitions]
red_app_1 [in Fsub_LetSum_Definitions]
red_app_1 [in Fsub_Definitions]
red_app_2 [in Fsub_Definitions]
red_app_2 [in Fsub_LetSum_Definitions]
red_case_inl [in Fsub_LetSum_Definitions]
red_case_inr [in Fsub_LetSum_Definitions]
red_case_1 [in Fsub_LetSum_Definitions]
red_inl_1 [in Fsub_LetSum_Definitions]
red_inr_1 [in Fsub_LetSum_Definitions]
red_let [in Fsub_LetSum_Definitions]
red_let_1 [in Fsub_LetSum_Definitions]
red_tabs [in Fsub_Definitions]
red_tabs [in Fsub_LetSum_Definitions]
red_tapp [in Fsub_Definitions]
red_tapp [in Fsub_LetSum_Definitions]
r_eval [in CoqIntro]
r_refl [in CoqIntro]
r_trans [in CoqIntro]
S
some_bool [in CoqIntro]some_nat [in CoqIntro]
sub_all [in Fsub_Definitions]
sub_all [in Fsub_LetSum_Definitions]
sub_arrow [in Fsub_LetSum_Definitions]
sub_arrow [in Fsub_Definitions]
sub_refl_tvar [in Fsub_LetSum_Definitions]
sub_refl_tvar [in Fsub_Definitions]
sub_sum [in Fsub_LetSum_Definitions]
sub_top [in Fsub_LetSum_Definitions]
sub_top [in Fsub_Definitions]
sub_trans_tvar [in Fsub_LetSum_Definitions]
sub_trans_tvar [in Fsub_Definitions]
T
tm_false [in CoqIntro]tm_if [in CoqIntro]
tm_iszero [in CoqIntro]
tm_pred [in CoqIntro]
tm_succ [in CoqIntro]
tm_true [in CoqIntro]
tm_zero [in CoqIntro]
type_all [in Fsub_LetSum_Definitions]
type_all [in Fsub_Definitions]
type_arrow [in Fsub_LetSum_Definitions]
type_arrow [in Fsub_Definitions]
type_sum [in Fsub_LetSum_Definitions]
type_top [in Fsub_LetSum_Definitions]
type_top [in Fsub_Definitions]
type_var [in Fsub_LetSum_Definitions]
type_var [in Fsub_Definitions]
typing_abs [in STLC_Solutions]
typing_abs [in Fsub_Definitions]
typing_abs [in Fsub_LetSum_Definitions]
typing_abs [in STLC_Tutorial]
typing_app [in STLC_Solutions]
typing_app [in Fsub_Definitions]
typing_app [in STLC_Tutorial]
typing_app [in Fsub_LetSum_Definitions]
typing_case [in Fsub_LetSum_Definitions]
typing_inl [in Fsub_LetSum_Definitions]
typing_inr [in Fsub_LetSum_Definitions]
typing_let [in Fsub_LetSum_Definitions]
typing_sub [in Fsub_Definitions]
typing_sub [in Fsub_LetSum_Definitions]
typing_tabs [in Fsub_Definitions]
typing_tabs [in Fsub_LetSum_Definitions]
typing_tapp [in Fsub_Definitions]
typing_tapp [in Fsub_LetSum_Definitions]
typing_var [in STLC_Tutorial]
typing_var [in Fsub_LetSum_Definitions]
typing_var [in Fsub_Definitions]
typing_var [in STLC_Solutions]
typ_all [in Fsub_LetSum_Definitions]
typ_all [in Fsub_Definitions]
typ_arrow [in Fsub_LetSum_Definitions]
typ_arrow [in Fsub_Definitions]
typ_arrow [in STLC_Tutorial]
typ_arrow [in STLC_Solutions]
typ_base [in STLC_Tutorial]
typ_base [in STLC_Solutions]
typ_bvar [in Fsub_LetSum_Definitions]
typ_bvar [in Fsub_Definitions]
typ_fvar [in Fsub_LetSum_Definitions]
typ_fvar [in Fsub_Definitions]
typ_sum [in Fsub_LetSum_Definitions]
typ_top [in Fsub_LetSum_Definitions]
typ_top [in Fsub_Definitions]
V
value_abs [in Fsub_LetSum_Definitions]value_abs [in Fsub_Definitions]
value_abs [in STLC_Tutorial]
value_abs [in STLC_Solutions]
value_inl [in Fsub_LetSum_Definitions]
value_inr [in Fsub_LetSum_Definitions]
value_tabs [in Fsub_LetSum_Definitions]
value_tabs [in Fsub_Definitions]
W
wf_env_empty [in Fsub_LetSum_Definitions]wf_env_empty [in Fsub_Definitions]
wf_env_sub [in Fsub_Definitions]
wf_env_sub [in Fsub_LetSum_Definitions]
wf_env_typ [in Fsub_LetSum_Definitions]
wf_env_typ [in Fsub_Definitions]
wf_typ_all [in Fsub_Definitions]
wf_typ_all [in Fsub_LetSum_Definitions]
wf_typ_arrow [in Fsub_Definitions]
wf_typ_arrow [in Fsub_LetSum_Definitions]
wf_typ_sum [in Fsub_LetSum_Definitions]
wf_typ_top [in Fsub_Definitions]
wf_typ_top [in Fsub_LetSum_Definitions]
wf_typ_var [in Fsub_Definitions]
wf_typ_var [in Fsub_LetSum_Definitions]
Inductive Index
B
binding [in Fsub_LetSum_Definitions]binding [in Fsub_Definitions]
bool_option [in CoqIntro]
bvalue [in CoqIntro]
D
Decide.FSetDecideAuxiliary.FSet_elt_Prop [in FSetDecide]Decide.FSetDecideAuxiliary.FSet_Prop [in FSetDecide]
E
eval [in STLC_Tutorial]eval [in CoqIntro]
eval [in STLC_Solutions]
eval_many [in CoqIntro]
eval_rtc [in CoqIntro]
exp [in Fsub_Definitions]
exp [in STLC_Tutorial]
exp [in STLC_Solutions]
exp [in Fsub_LetSum_Definitions]
expr [in Fsub_LetSum_Definitions]
expr [in Fsub_Definitions]
F
full_eval [in CoqIntro]L
lc [in STLC_Tutorial]lc [in STLC_Solutions]
N
nat_option [in CoqIntro]nvalue [in CoqIntro]
O
ok [in Environment]R
red [in Fsub_Definitions]red [in Fsub_LetSum_Definitions]
S
sub [in Fsub_LetSum_Definitions]sub [in Fsub_Definitions]
T
tm [in CoqIntro]typ [in Fsub_LetSum_Definitions]
typ [in Fsub_Definitions]
typ [in STLC_Solutions]
typ [in STLC_Tutorial]
type [in Fsub_Definitions]
type [in Fsub_LetSum_Definitions]
typing [in STLC_Solutions]
typing [in Fsub_Definitions]
typing [in Fsub_LetSum_Definitions]
typing [in STLC_Tutorial]
V
value [in Fsub_LetSum_Definitions]value [in STLC_Tutorial]
value [in Fsub_Definitions]
value [in STLC_Solutions]
W
wf_env [in Fsub_Definitions]wf_env [in Fsub_LetSum_Definitions]
wf_typ [in Fsub_LetSum_Definitions]
wf_typ [in Fsub_Definitions]
Definition Index
A
ATOM.Atom_as_OT.t [in Atom]B
binds [in Environment]body_e [in Fsub_LetSum_Definitions]
bool_to_tm [in CoqIntro]
D
demo_rep1 [in STLC_Solutions]demo_rep1 [in STLC_Tutorial]
demo_rep2 [in STLC_Solutions]
demo_rep2 [in STLC_Tutorial]
dom [in Environment]
F
fv [in STLC_Tutorial]fv [in STLC_Solutions]
fv_ee [in Fsub_Infrastructure]
fv_ee [in Fsub_LetSum_Infrastructure]
fv_te [in Fsub_LetSum_Infrastructure]
fv_te [in Fsub_Infrastructure]
fv_tt [in Fsub_LetSum_Infrastructure]
fv_tt [in Fsub_Infrastructure]
G
get [in Environment]I
interp [in CoqIntro]is_bool [in CoqIntro]
M
map [in Environment]N
nat_to_tm [in CoqIntro]normal_form [in CoqIntro]
O
open [in STLC_Tutorial]open [in STLC_Solutions]
open_ee [in Fsub_LetSum_Definitions]
open_ee [in Fsub_Definitions]
open_ee_rec [in Fsub_LetSum_Definitions]
open_ee_rec [in Fsub_Definitions]
open_rec [in STLC_Solutions]
open_rec [in STLC_Tutorial]
open_te [in Fsub_LetSum_Definitions]
open_te [in Fsub_Definitions]
open_te_rec [in Fsub_Definitions]
open_te_rec [in Fsub_LetSum_Definitions]
open_tt [in Fsub_Definitions]
open_tt [in Fsub_LetSum_Definitions]
open_tt_rec [in Fsub_LetSum_Definitions]
open_tt_rec [in Fsub_Definitions]
S
singleton_list [in Environment]strongly_diverges [in CoqIntro]
subst [in STLC_Solutions]
subst [in STLC_Tutorial]
subst_ee [in Fsub_Infrastructure]
subst_ee [in Fsub_LetSum_Infrastructure]
subst_tb [in Fsub_LetSum_Infrastructure]
subst_tb [in Fsub_Infrastructure]
subst_te [in Fsub_LetSum_Infrastructure]
subst_te [in Fsub_Infrastructure]
subst_tt [in Fsub_LetSum_Infrastructure]
subst_tt [in Fsub_Infrastructure]
T
tm_to_bool [in CoqIntro]tm_to_nat [in CoqIntro]
transitivity_on [in Fsub_LetSum_Soundness]
transitivity_on [in Fsub_Soundness]
two [in STLC_Solutions]
V
value [in CoqIntro]Module Index
A
ATOM [in Atom]AtomImpl [in Atom]
AtomSet [in Atom]
Atom_as_OT [in Atom]
D
Decide [in FSetDecide]E
E [in FiniteSets]F
F [in FiniteSets]FSetDecideAuxiliary [in FSetDecide]
FSetDecideTestCases [in FSetDecide]
FSetLogicalFacts [in FSetDecide]
M
Make [in FiniteSets]N
Notin [in FSetNotin]S
S [in FiniteSets]Library Index
A
AdditionalTacticsAtom
C
CoqIntroE
EnvironmentF
FiniteSetsFSetDecide
FSetNotin
Fsub_Definitions
Fsub_Infrastructure
Fsub_Lemmas
Fsub_LetSum_Definitions
Fsub_LetSum_Infrastructure
Fsub_LetSum_Lemmas
Fsub_LetSum_Soundness
Fsub_Soundness
L
ListFactsM
MetatheoryS
STLC_SolutionsSTLC_Tutorial
| 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 | _ | (756 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 | _ | (8 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 | _ | (416 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 | _ | (197 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 | _ | (46 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 | _ | (57 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 | _ | (13 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 | _ | (19 entries) |
This page has been generated by coqdoc