| 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 | _ | (1294 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 | _ | (391 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 | _ | (348 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 | _ | (101 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 | _ | (42 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 | _ | (371 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 | _ | (27 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 | _ | (14 entries) |
Global Index
A
abs_arrow [lemma, in Subtyping]add_slowly [definition, in Hoare]
admit [definition, in Basics]
aequiv [definition, in Equiv]
aequiv_example [lemma, in Equiv]
aeval [definition, in Imp]
AExp [module, in Imp]
aexp [inductive, in Imp]
AExp.aeval [definition, in Imp]
AExp.aexp [inductive, in Imp]
AExp.AMinus [constructor, in Imp]
AExp.AMult [constructor, in Imp]
AExp.ANum [constructor, in Imp]
AExp.APlus [constructor, in Imp]
AExp.A0 [abbreviation, in Imp]
AExp.A1 [abbreviation, in Imp]
AExp.A2 [abbreviation, in Imp]
AExp.A3 [abbreviation, in Imp]
AExp.A4 [abbreviation, in Imp]
AExp.A5 [abbreviation, in Imp]
AExp.BAnd [constructor, in Imp]
AExp.BEq [constructor, in Imp]
AExp.beval [definition, in Imp]
AExp.bexp [inductive, in Imp]
AExp.BFalse [constructor, in Imp]
AExp.BLe [constructor, in Imp]
AExp.BNot [constructor, in Imp]
AExp.BOr [constructor, in Imp]
AExp.BTrue [constructor, in Imp]
AExp.foo [lemma, in Imp]
AExp.foo' [lemma, in Imp]
AExp.foo'' [lemma, in Imp]
AExp.optimize_0plus [definition, in Imp]
AExp.optimize_0plus_sound [lemma, in Imp]
AExp.optimize_0plus_sound' [lemma, in Imp]
AExp.optimize_0plus_sound'' [lemma, in Imp]
AExp.test_aeval1 [definition, in Imp]
AExp.test_optimize_0plus [definition, in Imp]
AExp.two_plus_two [definition, in Imp]
AExp.two_plus_two' [definition, in Imp]
afi_abs [constructor, in Subtyping]
afi_app1 [constructor, in Subtyping]
afi_app2 [constructor, in Subtyping]
afi_proj [constructor, in Subtyping]
afi_rhead [constructor, in Subtyping]
afi_rtail [constructor, in Subtyping]
afi_var [constructor, in Subtyping]
AId [constructor, in Imp]
all3_spec [lemma, in Basics]
AMinus [constructor, in Imp]
AMult [constructor, in Imp]
and [inductive, in Logic]
andb [definition, in Basics]
andb3 [definition, in Basics]
andb_false [lemma, in Logic]
andb_false_r [lemma, in Basics]
andb_true [lemma, in Logic]
andb_true [lemma, in SfLib]
andb_true_elim1 [lemma, in SfLib]
andb_true_elim1 [lemma, in Basics]
andb_true_elim2 [lemma, in SfLib]
andb_true_elim2 [lemma, in Basics]
and_assoc [lemma, in Logic]
and_commut [lemma, in Logic]
and_example [lemma, in Logic]
and_example' [lemma, in Logic]
antisymmetric [definition, in Logic]
ANum [constructor, in Imp]
APlus [constructor, in Imp]
app [definition, in Poly]
appears_free_in [inductive, in Subtyping]
Assertion [definition, in Hoare]
assn_sub [definition, in Hoare]
assn_sub_example [definition, in Hoare]
assn_sub_example' [definition, in Hoare]
atrans_sound [definition, in Equiv]
auto_example_1 [lemma, in Stlc]
auto_example_2 [lemma, in Stlc]
auto_example_3 [lemma, in Stlc]
A0 [abbreviation, in Imp]
A1 [abbreviation, in Imp]
A2 [abbreviation, in Imp]
A3 [abbreviation, in Imp]
A4 [abbreviation, in Imp]
A5 [abbreviation, in Imp]
A6 [abbreviation, in Imp]
B
BAnd [constructor, in Imp]Basics [library]
bassn [definition, in Hoare]
BEq [constructor, in Imp]
bequiv [definition, in Equiv]
bequiv_example [lemma, in Equiv]
beq_false_not_eq [lemma, in Logic]
beq_id [definition, in Imp]
beq_id_eq [lemma, in Imp]
beq_id_false_not_eq [lemma, in Imp]
beq_id_refl [lemma, in Imp]
beq_nat [definition, in Basics]
beq_nat_eq [lemma, in Poly]
beq_nat_eq' [lemma, in Poly]
beq_nat_refl [lemma, in Basics]
beq_nat_sym [definition, in Lists]
beq_nat_trans [lemma, in Poly]
beq_nat_0_l [lemma, in Poly]
beq_nat_0_r [lemma, in Poly]
between [definition, in Props]
beval [definition, in Imp]
bexp [inductive, in Imp]
bexp_eval_false [lemma, in Hoare]
bexp_eval_true [lemma, in Hoare]
BFalse [constructor, in Imp]
bind_option [definition, in Imp]
BLe [constructor, in Imp]
ble_nat [definition, in Basics]
ble_nat [definition, in SfLib]
ble_nat_false [lemma, in Logic]
ble_nat_false [lemma, in SfLib]
ble_nat_n_Sn_false [lemma, in Logic]
ble_nat_refl [lemma, in Basics]
ble_nat_true [lemma, in Logic]
ble_nat_true [lemma, in SfLib]
blt_nat [definition, in Basics]
blue [constructor, in Props]
BNot [constructor, in Imp]
bool [inductive, in Basics]
boollist [inductive, in Poly]
bool_cons [constructor, in Poly]
bool_nil [constructor, in Poly]
BOr [constructor, in Imp]
btrans_sound [definition, in Equiv]
BTrue [constructor, in Imp]
bvalue [inductive, in Stlc]
bv_false [constructor, in Stlc]
bv_true [constructor, in Stlc]
C
canonical_forms_of_arrow_types [lemma, in Subtyping]CAss [constructor, in Imp]
CAss_congruence [lemma, in Equiv]
CEAss [constructor, in Imp]
CEIfFalse [constructor, in Imp]
CEIfTrue [constructor, in Imp]
cequiv [definition, in Equiv]
cequiv_state [lemma, in Equiv]
CESeq [constructor, in Imp]
CESkip [constructor, in Imp]
ceval [inductive, in Imp]
ceval_and_ceval_step_coincide [lemma, in Imp]
ceval_deterministic [lemma, in Equiv]
ceval_deterministic' [lemma, in Equiv]
ceval_example1 [definition, in Imp]
ceval_example2 [definition, in Imp]
ceval_step [definition, in Imp]
ceval_step1 [definition, in Imp]
ceval_step2 [definition, in Imp]
ceval_step_more [lemma, in Imp]
ceval_step__ceval [lemma, in Imp]
ceval__ceval_step [lemma, in Imp]
CEWhileEnd [constructor, in Imp]
CEWhileLoop [constructor, in Imp]
CIf [constructor, in Imp]
CIf_congruence [lemma, in Equiv]
CIf_false [lemma, in Equiv]
CIf_true [lemma, in Equiv]
CIf_true_simple [lemma, in Equiv]
classic [definition, in Logic]
com [inductive, in Imp]
combine [definition, in Poly]
Combined [module, in Smallstep]
Combined.step [inductive, in Smallstep]
Combined.ST_If [constructor, in Smallstep]
Combined.ST_IfFalse [constructor, in Smallstep]
Combined.ST_IfTrue [constructor, in Smallstep]
Combined.ST_PlusConstConst [constructor, in Smallstep]
Combined.ST_Plus1 [constructor, in Smallstep]
Combined.ST_Plus2 [constructor, in Smallstep]
Combined.tm [inductive, in Smallstep]
Combined.tm_const [constructor, in Smallstep]
Combined.tm_false [constructor, in Smallstep]
Combined.tm_if [constructor, in Smallstep]
Combined.tm_plus [constructor, in Smallstep]
Combined.tm_true [constructor, in Smallstep]
Combined.value [inductive, in Smallstep]
Combined.v_const [constructor, in Smallstep]
Combined.v_false [constructor, in Smallstep]
Combined.v_true [constructor, in Smallstep]
conj [constructor, in Logic]
cons [constructor, in Poly]
constfun [definition, in Poly]
context [definition, in Subtyping]
context_invariance [lemma, in Subtyping]
contradiction_implies_anything [lemma, in Logic]
contrapositive [lemma, in Logic]
countoddmembers' [definition, in Poly]
CSeq [constructor, in Imp]
CSeq_congruence [lemma, in Equiv]
CSkip [constructor, in Imp]
ctrans_sound [definition, in Equiv]
curry_uncurry [lemma, in Poly]
CWhile [constructor, in Imp]
CWhile_congruence [lemma, in Equiv]
CWhile_false [lemma, in Equiv]
CWhile_true [lemma, in Equiv]
CWhile_true_nonterm [lemma, in Equiv]
C1 [constructor, in Props]
C2 [constructor, in Props]
D
day [inductive, in Basics]de_morgan_not_and_not [definition, in Logic]
dist_exists_or [lemma, in Logic]
dist_not_exists [lemma, in Logic]
doit3times [definition, in Poly]
double [definition, in Poly]
double_even [lemma, in Props]
double_injective [lemma, in Poly]
double_injective' [lemma, in Props]
double_injective_FAILED [lemma, in Props]
double_injective_take2 [lemma, in Props]
double_injective_take2_FAILED [lemma, in Props]
double_neg [lemma, in Logic]
E
empty [definition, in Subtyping]empty_state [definition, in Imp]
eqnat_false_S [lemma, in Props]
Equiv [library]
equivalence [definition, in Logic]
eq_add_S [lemma, in Poly]
ev [inductive, in Props]
ev [inductive, in SfLib]
eval [inductive, in Smallstep]
eval__stepmany [lemma, in Smallstep]
eval__value [lemma, in Smallstep]
even [definition, in Props]
evenb [definition, in Basics]
evenb_n__oddb_Sn [lemma, in Basics]
even5_nonsense [lemma, in Props]
even_ev [lemma, in Logic]
even_n__even_SSn [definition, in Props]
ev_even [lemma, in Props]
ev_even' [lemma, in Props]
ev_ev_even [lemma, in Props]
ev_minus2 [lemma, in Props]
ev_minus2' [lemma, in Props]
ev_MyProp [lemma, in Props]
ev_MyProp' [lemma, in Props]
ev_not_ev_S [lemma, in Logic]
ev_not_ev_S [lemma, in SfLib]
ev_plus4 [definition, in Props]
ev_plus4' [lemma, in Props]
ev_SS [constructor, in Props]
ev_SS [constructor, in SfLib]
ev_sum [lemma, in Props]
ev_ten [definition, in Props]
ev_0 [constructor, in Props]
ev_0 [constructor, in SfLib]
ex [inductive, in Logic]
Examples [module, in Subtyping]
Examples.A [abbreviation, in Subtyping]
Examples.B [abbreviation, in Subtyping]
Examples.C [abbreviation, in Subtyping]
Examples.i [abbreviation, in Subtyping]
Examples.j [abbreviation, in Subtyping]
Examples.k [abbreviation, in Subtyping]
Examples.subtyping_example_0 [definition, in Subtyping]
Examples.subtyping_example_1 [definition, in Subtyping]
Examples.subtyping_example_2 [definition, in Subtyping]
Examples.subtyping_example_3 [definition, in Subtyping]
Examples.subtyping_example_4 [definition, in Subtyping]
Examples.tm_rcd_kj [definition, in Subtyping]
Examples.ty_rcd_j [definition, in Subtyping]
Examples.ty_rcd_kj [definition, in Subtyping]
Examples.x [abbreviation, in Subtyping]
Examples.y [abbreviation, in Subtyping]
Examples.z [abbreviation, in Subtyping]
Examples2 [module, in Subtyping]
Examples2.typing_example_0 [definition, in Subtyping]
Examples2.typing_example_1 [definition, in Subtyping]
Examples2.typing_example_2 [definition, in Subtyping]
Excerpt_From_Coq_Relations_Library [module, in Smallstep]
Excerpt_From_Coq_Relations_Library.clos_refl_trans [inductive, in Smallstep]
Excerpt_From_Coq_Relations_Library.rt_refl [constructor, in Smallstep]
Excerpt_From_Coq_Relations_Library.rt_step [constructor, in Smallstep]
Excerpt_From_Coq_Relations_Library.rt_trans [constructor, in Smallstep]
excluded_middle [definition, in Logic]
exists_example_1 [definition, in Logic]
exists_example_1' [definition, in Logic]
exists_example_2 [lemma, in Logic]
exp [definition, in Basics]
exp_body [definition, in Imp]
extend [definition, in Subtyping]
ex_falso_quodlibet [lemma, in SfLib]
ex_falso_quodlibet [lemma, in Logic]
ex_intro [constructor, in Logic]
E_Const [constructor, in Smallstep]
E_Plus [constructor, in Smallstep]
F
factorial [definition, in Basics]Factorial [module, in Hoare]
Factorial.fact_body [definition, in Hoare]
Factorial.fact_com [definition, in Hoare]
Factorial.fact_com_correct [lemma, in Hoare]
Factorial.fact_loop [definition, in Hoare]
Factorial.real_fact [definition, in Hoare]
fact_body [definition, in Imp]
fact_body_preserves_invariant [lemma, in Equiv]
fact_com [definition, in Imp]
fact_com_correct [lemma, in Equiv]
fact_invariant [definition, in Equiv]
fact_loop [definition, in Imp]
fact_loop_preserves_invariant [lemma, in Equiv]
failed_proof [lemma, in Props]
false [constructor, in Basics]
False [inductive, in Logic]
False_implies_nonsense [lemma, in Logic]
filter [definition, in Poly]
filter_exercise [lemma, in Poly]
find_parity [definition, in Hoare]
find_parity_correct [lemma, in Hoare]
find_parity_invariant [definition, in Hoare]
find_parity_invariant' [definition, in Hoare]
FirstLe [module, in Logic]
FirstLe.le [inductive, in Logic]
FirstLe.le_n [constructor, in Logic]
FirstLe.le_S [constructor, in Logic]
FirstTry [module, in MoreStlc]
five_not_even [lemma, in Logic]
flat_map [definition, in Poly]
fold [definition, in Poly]
fold_aexp_ex1 [definition, in Equiv]
fold_aexp_ex2 [definition, in Equiv]
fold_bexp_ex1 [definition, in Equiv]
fold_bexp_ex2 [definition, in Equiv]
fold_com_ex1 [definition, in Equiv]
fold_constants_aexp [definition, in Equiv]
fold_constants_aexp_sound [lemma, in Equiv]
fold_constants_aexp_sound' [lemma, in Equiv]
fold_constants_bexp [definition, in Equiv]
fold_constants_bexp_sound [lemma, in Equiv]
fold_constants_com [definition, in Equiv]
fold_constants_com_sound [lemma, in Equiv]
foo' [inductive, in Props]
four_ev [definition, in Props]
four_ev' [lemma, in Props]
free_in_context [lemma, in Subtyping]
friday [constructor, in Basics]
fst [definition, in Poly]
G
green [constructor, in Props]guard_false_after_loop [lemma, in Equiv]
H
has_type [inductive, in Subtyping]has_type [inductive, in Stlc]
has_type_nonexample [definition, in Stlc]
has_type_1 [definition, in Stlc]
has_type__wf [lemma, in Subtyping]
hd_opt [definition, in Poly]
Hoare [library]
hoare_asgn [lemma, in Hoare]
hoare_asgn_eq [lemma, in Hoare]
hoare_asgn_example1 [definition, in Hoare]
hoare_asgn_example1' [definition, in Hoare]
hoare_asgn_example2 [definition, in Hoare]
hoare_asgn_example3 [definition, in Hoare]
hoare_asgn_example4 [definition, in Hoare]
hoare_consequence [lemma, in Hoare]
hoare_consequence_post [lemma, in Hoare]
hoare_consequence_pre [lemma, in Hoare]
hoare_if [lemma, in Hoare]
hoare_post_true [lemma, in Hoare]
hoare_pre_false [lemma, in Hoare]
hoare_seq [lemma, in Hoare]
hoare_skip [lemma, in Hoare]
hoare_triple [definition, in Hoare]
hoare_while [lemma, in Hoare]
I
id [inductive, in Imp]Id [constructor, in Imp]
iff [definition, in Logic]
iff_implies [lemma, in Logic]
iff_refl [lemma, in Logic]
iff_sym [lemma, in Logic]
iff_trans [lemma, in Logic]
iff_trans [lemma, in Equiv]
if_exercise [definition, in Hoare]
Imp [library]
implies_to_or [definition, in Logic]
index [definition, in Poly]
index_after_last [lemma, in Props]
inequiv_exercise [lemma, in Equiv]
L
le [inductive, in Logic]leaf [constructor, in Props]
length [definition, in Poly]
length' [definition, in Poly]
length_appendtwice [lemma, in Props]
length_append_cons [lemma, in Props]
length_snoc' [lemma, in Poly]
length_snoc'' [lemma, in Poly]
length_snoc''' [lemma, in Props]
le_antisymmetric [lemma, in Logic]
le_n [constructor, in Logic]
le_not_a_partial_function [lemma, in Logic]
le_not_symmetric [lemma, in Logic]
le_order [lemma, in Logic]
le_plus_l [lemma, in Logic]
le_reflexive [lemma, in Logic]
le_S [constructor, in Logic]
le_Sn_le [lemma, in Logic]
le_Sn_n [lemma, in Logic]
le_step [lemma, in Logic]
le_S_n [lemma, in Logic]
le_trans [lemma, in Logic]
list [inductive, in Poly]
Lists [library]
Logic [library]
lookup_field_in_value [lemma, in Subtyping]
loop [definition, in Imp]
loop_never_stops [lemma, in Imp]
loop_unrolling [lemma, in Equiv]
lt [definition, in Logic]
lt_S [lemma, in Logic]
lt_trans [lemma, in Logic]
lt_trans' [lemma, in Logic]
lt_trans'' [lemma, in Logic]
l_123 [definition, in Poly]
l_123' [definition, in Poly]
l_123'' [definition, in Poly]
M
map [definition, in Poly]map_option [definition, in Poly]
map_rev [lemma, in Poly]
minustwo [definition, in Basics]
minus_diag [lemma, in Basics]
minus_pred [lemma, in Hoare]
minus_0_n [lemma, in Hoare]
monday [constructor, in Basics]
MoreStlc [library]
mult_assoc [lemma, in Basics]
mult_comm [lemma, in Basics]
mult_plus_distr_r [lemma, in Basics]
mult_0_l [lemma, in Basics]
mult_0_plus [lemma, in Basics]
mult_0_plus' [lemma, in Basics]
mult_0_r [lemma, in Basics]
mult_0_r' [lemma, in Props]
mult_0_r'' [lemma, in Props]
mult_1_l [lemma, in Basics]
mult_1_plus [lemma, in Basics]
MumbleBaz [module, in Poly]
MumbleBaz.a [constructor, in Poly]
MumbleBaz.b [constructor, in Poly]
MumbleBaz.baz [inductive, in Poly]
MumbleBaz.c [constructor, in Poly]
MumbleBaz.d [constructor, in Poly]
MumbleBaz.e [constructor, in Poly]
MumbleBaz.grumble [inductive, in Poly]
MumbleBaz.mumble [inductive, in Poly]
MumbleBaz.x [constructor, in Poly]
MumbleBaz.y [constructor, in Poly]
MyEquality [module, in Logic]
MyEquality.eq [inductive, in Logic]
MyEquality.eq' [inductive, in Logic]
MyEquality.refl_equal [constructor, in Logic]
MyEquality.refl_equal' [constructor, in Logic]
MyEquality.two_defs_of_eq_coincide [lemma, in Logic]
mynil [definition, in Poly]
MyProp [inductive, in Props]
MyProp1 [constructor, in Props]
MyProp2 [constructor, in Props]
MyProp3 [constructor, in Props]
MyProp_ev [lemma, in Props]
MyProp_iff_ev [definition, in Logic]
MyProp_plustwo [lemma, in Props]
MyProp_ten [lemma, in Props]
MyProp_0 [lemma, in Props]
N
nandb [definition, in Basics]natlist [inductive, in Props]
NatList [module, in Lists]
NatList.add [definition, in Lists]
NatList.alternate [definition, in Lists]
NatList.app [definition, in Lists]
NatList.append_snoc [lemma, in Lists]
NatList.app_length [lemma, in Lists]
NatList.app_nil_end [lemma, in Lists]
NatList.ass_app [lemma, in Lists]
NatList.ass_app' [lemma, in Lists]
NatList.ass_app4 [lemma, in Lists]
NatList.bag [definition, in Lists]
NatList.beq_natlist [definition, in Lists]
NatList.beq_natlist_refl [lemma, in Lists]
NatList.beq_nat_sym [lemma, in Lists]
NatList.ble_n_Sn [lemma, in Lists]
NatList.cons [constructor, in Lists]
NatList.count [definition, in Lists]
NatList.countoddmembers [definition, in Lists]
NatList.count_member_nonzero [lemma, in Lists]
NatList.distr_rev [lemma, in Lists]
NatList.fst [definition, in Lists]
NatList.fst' [definition, in Lists]
NatList.fst_swap_is_snd [lemma, in Lists]
NatList.hd [definition, in Lists]
NatList.hd_opt [definition, in Lists]
NatList.index [definition, in Lists]
NatList.index' [definition, in Lists]
NatList.index_bad [definition, in Lists]
NatList.length [definition, in Lists]
NatList.length_snoc [lemma, in Lists]
NatList.l_123 [definition, in Lists]
NatList.l_123' [definition, in Lists]
NatList.l_123'' [definition, in Lists]
NatList.l_123''' [definition, in Lists]
NatList.member [definition, in Lists]
NatList.natlist [inductive, in Lists]
NatList.natoption [inductive, in Lists]
NatList.natprod [inductive, in Lists]
NatList.nil [constructor, in Lists]
NatList.nil_app [lemma, in Lists]
NatList.None [constructor, in Lists]
NatList.nonzeros [definition, in Lists]
NatList.nonzeros_length [lemma, in Lists]
NatList.oddmembers [definition, in Lists]
NatList.option_elim [definition, in Lists]
NatList.option_elim_hd [lemma, in Lists]
NatList.pair [constructor, in Lists]
NatList.remove_all [definition, in Lists]
NatList.remove_decreases_count [lemma, in Lists]
NatList.remove_one [definition, in Lists]
NatList.repeat [definition, in Lists]
NatList.rev [definition, in Lists]
NatList.rev_exercise1 [lemma, in Lists]
NatList.rev_involutive [lemma, in Lists]
NatList.rev_length [lemma, in Lists]
NatList.rev_length_firsttry [lemma, in Lists]
NatList.silly1 [lemma, in Lists]
NatList.silly2 [lemma, in Lists]
NatList.silly2a [lemma, in Lists]
NatList.silly3 [lemma, in Lists]
NatList.silly3_firsttry [lemma, in Lists]
NatList.silly_ex [lemma, in Lists]
NatList.snd [definition, in Lists]
NatList.snd' [definition, in Lists]
NatList.snd_fst_is_swap [lemma, in Lists]
NatList.snoc [definition, in Lists]
NatList.snoc_append [lemma, in Lists]
NatList.Some [constructor, in Lists]
NatList.subset [definition, in Lists]
NatList.surjective_pairing [lemma, in Lists]
NatList.surjective_pairing' [lemma, in Lists]
NatList.surjective_pairing_stuck [lemma, in Lists]
NatList.swap_pair [definition, in Lists]
NatList.sym_eq_bool [lemma, in Lists]
NatList.test_add1 [definition, in Lists]
NatList.test_add2 [definition, in Lists]
NatList.test_alternate1 [definition, in Lists]
NatList.test_alternate2 [definition, in Lists]
NatList.test_alternate3 [definition, in Lists]
NatList.test_app1 [definition, in Lists]
NatList.test_app2 [definition, in Lists]
NatList.test_app3 [definition, in Lists]
NatList.test_beq_natlist1 [definition, in Lists]
NatList.test_beq_natlist2 [definition, in Lists]
NatList.test_beq_natlist3 [definition, in Lists]
NatList.test_countoddmembers1 [definition, in Lists]
NatList.test_countoddmembers2 [definition, in Lists]
NatList.test_countoddmembers3 [definition, in Lists]
NatList.test_count1 [definition, in Lists]
NatList.test_count2 [definition, in Lists]
NatList.test_hd_opt1 [definition, in Lists]
NatList.test_hd_opt2 [definition, in Lists]
NatList.test_hd_opt3 [definition, in Lists]
NatList.test_index1 [definition, in Lists]
NatList.test_index2 [definition, in Lists]
NatList.test_index3 [definition, in Lists]
NatList.test_member1 [definition, in Lists]
NatList.test_member2 [definition, in Lists]
NatList.test_nonzeros [definition, in Lists]
NatList.test_oddmembers [definition, in Lists]
NatList.test_remove_all1 [definition, in Lists]
NatList.test_remove_all2 [definition, in Lists]
NatList.test_remove_all3 [definition, in Lists]
NatList.test_remove_all4 [definition, in Lists]
NatList.test_remove_one1 [definition, in Lists]
NatList.test_remove_one2 [definition, in Lists]
NatList.test_remove_one3 [definition, in Lists]
NatList.test_remove_one4 [definition, in Lists]
NatList.test_rev1 [definition, in Lists]
NatList.test_rev2 [definition, in Lists]
NatList.test_subset1 [definition, in Lists]
NatList.test_subset2 [definition, in Lists]
NatList.test_union1 [definition, in Lists]
NatList.tl [definition, in Lists]
NatList.tl_length_pred [lemma, in Lists]
NatList.union [definition, in Lists]
natlist1 [inductive, in Props]
nat_induction [definition, in Props]
nat_induction_example [definition, in Props]
ncons [constructor, in Props]
negb [definition, in Basics]
negb_involutive [lemma, in Basics]
neq0_not_true__eq_0 [lemma, in Hoare]
neq0_true__eq_S [lemma, in Hoare]
next_even [inductive, in Logic]
next_nat [inductive, in Smallstep]
next_nat [inductive, in Logic]
next_nat_closure_is_le [lemma, in Smallstep]
next_nat_partial_function [lemma, in Logic]
next_weekday [definition, in Basics]
ne_1 [constructor, in Logic]
ne_2 [constructor, in Logic]
nf_is_value [lemma, in Smallstep]
nil [constructor, in Poly]
nil_app [lemma, in Poly]
nn [constructor, in Logic]
nn [constructor, in Smallstep]
nnil [constructor, in Props]
nnil1 [constructor, in Props]
no [constructor, in Props]
node [constructor, in Props]
None [constructor, in Poly]
nonsense_implies_False [lemma, in Logic]
normalizing [definition, in Smallstep]
normal_form [definition, in Smallstep]
normal_forms_unique [lemma, in Smallstep]
normal_form_of [definition, in Smallstep]
not [definition, in Logic]
not_both_true_and_false [lemma, in Logic]
not_eq_beq_false [lemma, in SfLib]
not_eq_beq_false [lemma, in Logic]
not_eq_beq_id_false [lemma, in Imp]
not_ev_ev_S [lemma, in Hoare]
not_ev_ev_S_gen [lemma, in Hoare]
not_False [lemma, in Logic]
not_false_then_true [lemma, in Logic]
no_whiles [definition, in Imp]
no_Whiles [inductive, in Imp]
no_whiles_eqv [lemma, in Imp]
nsnoc1 [constructor, in Props]
nvalue [inductive, in Stlc]
nv_succ [constructor, in Stlc]
nv_zero [constructor, in Stlc]
n_le_m__Sn_le_Sm [lemma, in Logic]
O
oddb [definition, in Basics]option [inductive, in Poly]
or [inductive, in Logic]
orb [definition, in Basics]
orb_false [lemma, in Logic]
orb_true [lemma, in Logic]
order [definition, in Logic]
or_commut [lemma, in Logic]
or_commut' [lemma, in Logic]
or_distributes_over_and [lemma, in Logic]
or_distributes_over_and_1 [lemma, in Logic]
or_distributes_over_and_2 [lemma, in Logic]
or_introl [constructor, in Logic]
or_intror [constructor, in Logic]
our_nat_induction_works [lemma, in Props]
our_nat_induction_works' [lemma, in Props]
override [definition, in Imp]
override [definition, in Poly]
override_eq [lemma, in Imp]
override_eq [lemma, in Poly]
override_example [lemma, in Imp]
override_example [lemma, in Poly]
override_neq [lemma, in Imp]
override_neq [lemma, in Poly]
override_permute [lemma, in Poly]
override_permute [lemma, in Imp]
override_same [lemma, in Imp]
override_same [lemma, in Poly]
override_shadow [lemma, in Poly]
override_shadow [lemma, in Imp]
O_le_n [lemma, in Logic]
P
P [module, in Props]pair [constructor, in Poly]
partial_function [definition, in SfLib]
partial_function [definition, in Logic]
peirce [definition, in Logic]
pexp [definition, in Imp]
Playground1 [module, in Basics]
Playground1.nat [inductive, in Basics]
Playground1.O [constructor, in Basics]
Playground1.pred [definition, in Basics]
Playground1.S [constructor, in Basics]
Playground2 [module, in Basics]
Playground2.minus [definition, in Basics]
Playground2.mult [definition, in Basics]
Playground2.plus [definition, in Basics]
plus2 [definition, in Imp]
plus2_notation [definition, in Imp]
plus2_spec [lemma, in Imp]
plus3 [definition, in Poly]
plus_assoc [lemma, in Basics]
plus_assoc' [lemma, in Props]
plus_assoc' [lemma, in Basics]
plus_ble_compat_l [lemma, in Basics]
plus_comm [lemma, in Basics]
plus_comm' [lemma, in Props]
plus_comm'' [lemma, in Props]
plus_fact [definition, in Props]
plus_fact_is_true [lemma, in Props]
plus_id_example [lemma, in Basics]
plus_id_exercise [lemma, in Basics]
plus_lt [lemma, in Logic]
plus_n_n_injective [lemma, in Poly]
plus_n_n_injective_take2 [lemma, in Props]
plus_n_Sm [lemma, in Basics]
plus_one_r' [lemma, in Props]
plus_one_r'' [lemma, in Props]
plus_O_n [lemma, in Basics]
plus_O_n' [lemma, in Basics]
plus_O_n'' [lemma, in Basics]
plus_rearrange_firsttry [lemma, in Basics]
plus_swap [lemma, in Basics]
plus_swap' [lemma, in Basics]
plus_0_r [lemma, in Basics]
plus_0_r_firsttry [lemma, in Basics]
plus_0_r_secondtry [lemma, in Basics]
plus_1_l [lemma, in Basics]
plus_1_neq_0 [lemma, in Basics]
plus_1_neq_0_firsttry [lemma, in Basics]
plus_2_2_is_4 [lemma, in Props]
Poly [library]
Preface [library]
preorder [definition, in Logic]
preservation [lemma, in Stlc]
preservation [lemma, in Subtyping]
preservation' [lemma, in Stlc]
preserved_by_S [definition, in Props]
prod [inductive, in Poly]
prod_curry [definition, in Poly]
prod_uncurry [definition, in Poly]
progress [lemma, in Stlc]
progress [lemma, in Smallstep]
progress [lemma, in Subtyping]
proj1 [lemma, in Logic]
proj2 [lemma, in Logic]
Props [library]
P.c1 [constructor, in Props]
P.c2 [constructor, in Props]
P.c3 [constructor, in Props]
P.p [inductive, in Props]
P_m0r [definition, in Props]
P_m0r' [definition, in Props]
R
R [module, in Logic]random_fact_1 [lemma, in Hoare]
random_fact_2 [lemma, in Hoare]
rcd_types_match [lemma, in Subtyping]
real_fact [definition, in Imp]
real_fact [definition, in Equiv]
record_tm [inductive, in Subtyping]
record_ty [inductive, in Subtyping]
red [constructor, in Props]
reduce_to_zero [definition, in Hoare]
reduce_to_zero_correct [lemma, in Hoare]
reflexive [definition, in Logic]
refl_aequiv [lemma, in Equiv]
refl_bequiv [lemma, in Equiv]
refl_cequiv [lemma, in Equiv]
refl_step_closure [inductive, in Smallstep]
relation [definition, in Logic]
repeat [definition, in Poly]
RepeatExercise [module, in Hoare]
RepeatExercise.CAss [constructor, in Hoare]
RepeatExercise.CEAss [constructor, in Hoare]
RepeatExercise.CEIfFalse [constructor, in Hoare]
RepeatExercise.CEIfTrue [constructor, in Hoare]
RepeatExercise.CESeq [constructor, in Hoare]
RepeatExercise.CESkip [constructor, in Hoare]
RepeatExercise.ceval [inductive, in Hoare]
RepeatExercise.CEWhileEnd [constructor, in Hoare]
RepeatExercise.CEWhileLoop [constructor, in Hoare]
RepeatExercise.CIf [constructor, in Hoare]
RepeatExercise.com [inductive, in Hoare]
RepeatExercise.CRepeat [constructor, in Hoare]
RepeatExercise.CSeq [constructor, in Hoare]
RepeatExercise.CSkip [constructor, in Hoare]
RepeatExercise.CWhile [constructor, in Hoare]
RepeatExercise.hoare_triple [definition, in Hoare]
rev [definition, in Poly]
rev_snoc [lemma, in Poly]
rgb [inductive, in Props]
rsc_R [lemma, in Smallstep]
rsc_refl [constructor, in Smallstep]
rsc_step [constructor, in Smallstep]
rsc_trans [lemma, in Smallstep]
rtc_rsc_coincide [lemma, in Smallstep]
rtm_cons [constructor, in Subtyping]
rtm_nil [constructor, in Subtyping]
rty_cons [constructor, in Subtyping]
rty_nil [constructor, in Subtyping]
R.c1 [constructor, in Logic]
R.c2 [constructor, in Logic]
R.c3 [constructor, in Logic]
R.c4 [constructor, in Logic]
R.c5 [constructor, in Logic]
R.R [inductive, in Logic]
S
saturday [constructor, in Basics]seq_assoc [lemma, in Equiv]
SfLib [library]
sillyex1 [definition, in Poly]
sillyex2 [definition, in Poly]
sillyfun [definition, in Poly]
sillyfun1 [definition, in Poly]
sillyfun1_odd [lemma, in Poly]
sillyfun1_odd_FAILED [lemma, in Poly]
sillyfun_false [lemma, in Poly]
silly3' [lemma, in Poly]
silly4 [lemma, in Poly]
silly5 [lemma, in Poly]
silly6 [lemma, in Poly]
silly7 [lemma, in Poly]
SimpleArith1 [module, in Smallstep]
SimpleArith1.eval [inductive, in Smallstep]
SimpleArith1.E_Const [constructor, in Smallstep]
SimpleArith1.E_Plus [constructor, in Smallstep]
SimpleArith2 [module, in Smallstep]
SimpleArith2.step [inductive, in Smallstep]
SimpleArith2.step_deterministic [lemma, in Smallstep]
SimpleArith2.ST_PlusConstConst [constructor, in Smallstep]
SimpleArith2.ST_Plus1 [constructor, in Smallstep]
SimpleArith2.ST_Plus2 [constructor, in Smallstep]
SimpleArith2.test_step_1 [definition, in Smallstep]
SimpleArith2.test_step_2 [definition, in Smallstep]
skip_left [lemma, in Equiv]
skip_right [lemma, in Equiv]
Smallstep [library]
snd [definition, in Poly]
snoc [definition, in Poly]
snoc_with_append [lemma, in Poly]
Some [constructor, in Poly]
some_tm_is_stuck [definition, in Stlc]
soundness [lemma, in Stlc]
sq [constructor, in Logic]
sqrt_com [definition, in Hoare]
sqrt_com_correct [lemma, in Hoare]
sqrt_inv [definition, in Hoare]
sqrt_loop [definition, in Hoare]
sqrt_spec [definition, in Hoare]
square_of [inductive, in Logic]
SSev_even [lemma, in Props]
SSev_ev_firsttry [lemma, in Props]
SSSSev_even [lemma, in Props]
ss_invariant [definition, in Equiv]
state [definition, in Imp]
step [inductive, in Smallstep]
step [inductive, in Subtyping]
step [inductive, in Stlc]
stepmany [abbreviation, in Smallstep]
stepmany [definition, in Stlc]
stepmany_congr_1 [lemma, in Smallstep]
stepmany_congr_2 [lemma, in Smallstep]
stepmany_iff_eval [lemma, in Smallstep]
stepmany__eval [lemma, in Smallstep]
step_deterministic [lemma, in Smallstep]
step_deterministic [lemma, in Stlc]
step_normalizing [lemma, in Smallstep]
step_normal_form [abbreviation, in Stlc]
step_normal_form [abbreviation, in Smallstep]
step_preserves_record_tm [lemma, in Subtyping]
step__eval [lemma, in Smallstep]
STLC [module, in Stlc]
Stlc [library]
STLCArith [module, in Stlc]
STLCArith.tm [inductive, in Stlc]
STLCArith.tm_abs [constructor, in Stlc]
STLCArith.tm_app [constructor, in Stlc]
STLCArith.tm_if0 [constructor, in Stlc]
STLCArith.tm_mult [constructor, in Stlc]
STLCArith.tm_nat [constructor, in Stlc]
STLCArith.tm_pred [constructor, in Stlc]
STLCArith.tm_succ [constructor, in Stlc]
STLCArith.tm_var [constructor, in Stlc]
STLCArith.ty [inductive, in Stlc]
STLCArith.ty_arrow [constructor, in Stlc]
STLCArith.ty_nat [constructor, in Stlc]
STLCChecker [module, in MoreStlc]
STLCChecker.beq_ty [definition, in MoreStlc]
STLCChecker.beq_ty_refl [lemma, in MoreStlc]
STLCChecker.beq_ty__eq [lemma, in MoreStlc]
STLCChecker.type_check [definition, in MoreStlc]
STLCChecker.type_checking_complete [lemma, in MoreStlc]
STLCChecker.type_checking_sound [lemma, in MoreStlc]
STLCExtended [module, in MoreStlc]
STLCExtended.a [abbreviation, in MoreStlc]
STLCExtended.A [abbreviation, in MoreStlc]
STLCExtended.afi_abs [constructor, in MoreStlc]
STLCExtended.afi_app1 [constructor, in MoreStlc]
STLCExtended.afi_app2 [constructor, in MoreStlc]
STLCExtended.afi_proj [constructor, in MoreStlc]
STLCExtended.afi_rhead [constructor, in MoreStlc]
STLCExtended.afi_rtail [constructor, in MoreStlc]
STLCExtended.afi_var [constructor, in MoreStlc]
STLCExtended.appears_free_in [inductive, in MoreStlc]
STLCExtended.B [abbreviation, in MoreStlc]
STLCExtended.context [definition, in MoreStlc]
STLCExtended.context_invariance [lemma, in MoreStlc]
STLCExtended.empty [definition, in MoreStlc]
STLCExtended.extend [definition, in MoreStlc]
STLCExtended.f [abbreviation, in MoreStlc]
STLCExtended.fact [definition, in MoreStlc]
STLCExtended.fact_example [definition, in MoreStlc]
STLCExtended.fact_typechecks [definition, in MoreStlc]
STLCExtended.FirstTry.alist [definition, in MoreStlc]
STLCExtended.FirstTry.ty [inductive, in MoreStlc]
STLCExtended.FirstTry.ty_arrow [constructor, in MoreStlc]
STLCExtended.FirstTry.ty_base [constructor, in MoreStlc]
STLCExtended.FirstTry.ty_rcd [constructor, in MoreStlc]
STLCExtended.free_in_context [lemma, in MoreStlc]
STLCExtended.g [abbreviation, in MoreStlc]
STLCExtended.has_type [inductive, in MoreStlc]
STLCExtended.has_type__wf [lemma, in MoreStlc]
STLCExtended.i1 [abbreviation, in MoreStlc]
STLCExtended.i2 [abbreviation, in MoreStlc]
STLCExtended.k [abbreviation, in MoreStlc]
STLCExtended.l [abbreviation, in MoreStlc]
STLCExtended.lookup_field_in_value [lemma, in MoreStlc]
STLCExtended.map [definition, in MoreStlc]
STLCExtended.map_example [definition, in MoreStlc]
STLCExtended.map_typechecks [definition, in MoreStlc]
STLCExtended.preservation [lemma, in MoreStlc]
STLCExtended.progress [lemma, in MoreStlc]
STLCExtended.record_tm [inductive, in MoreStlc]
STLCExtended.record_ty [inductive, in MoreStlc]
STLCExtended.rtm_cons [constructor, in MoreStlc]
STLCExtended.rtm_nil [constructor, in MoreStlc]
STLCExtended.rty_cons [constructor, in MoreStlc]
STLCExtended.rty_nil [constructor, in MoreStlc]
STLCExtended.step [inductive, in MoreStlc]
STLCExtended.stepmany [abbreviation, in MoreStlc]
STLCExtended.step_preserves_record_tm [lemma, in MoreStlc]
STLCExtended.ST_AppAbs [constructor, in MoreStlc]
STLCExtended.ST_App1 [constructor, in MoreStlc]
STLCExtended.ST_App2 [constructor, in MoreStlc]
STLCExtended.ST_ProjRcd [constructor, in MoreStlc]
STLCExtended.ST_Proj1 [constructor, in MoreStlc]
STLCExtended.ST_Rcd_Head [constructor, in MoreStlc]
STLCExtended.ST_Rcd_Tail [constructor, in MoreStlc]
STLCExtended.subst [definition, in MoreStlc]
STLCExtended.substitution_preserves_typing [lemma, in MoreStlc]
STLCExtended.tm [inductive, in MoreStlc]
STLCExtended.tm_abs [constructor, in MoreStlc]
STLCExtended.tm_app [constructor, in MoreStlc]
STLCExtended.tm_case [constructor, in MoreStlc]
STLCExtended.tm_cons [constructor, in MoreStlc]
STLCExtended.tm_fix [constructor, in MoreStlc]
STLCExtended.tm_fst [constructor, in MoreStlc]
STLCExtended.tm_if0 [constructor, in MoreStlc]
STLCExtended.tm_let [constructor, in MoreStlc]
STLCExtended.tm_lookup [definition, in MoreStlc]
STLCExtended.tm_mult [constructor, in MoreStlc]
STLCExtended.tm_nat [constructor, in MoreStlc]
STLCExtended.tm_nil [constructor, in MoreStlc]
STLCExtended.tm_pair [constructor, in MoreStlc]
STLCExtended.tm_pred [constructor, in MoreStlc]
STLCExtended.tm_proj [constructor, in MoreStlc]
STLCExtended.tm_rcons [constructor, in MoreStlc]
STLCExtended.tm_rnil [constructor, in MoreStlc]
STLCExtended.tm_snd [constructor, in MoreStlc]
STLCExtended.tm_succ [constructor, in MoreStlc]
STLCExtended.tm_var [constructor, in MoreStlc]
STLCExtended.ty [inductive, in MoreStlc]
STLCExtended.typing_example [definition, in MoreStlc]
STLCExtended.typing_example_2 [lemma, in MoreStlc]
STLCExtended.typing_nonexample [definition, in MoreStlc]
STLCExtended.typing_nonexample_2 [definition, in MoreStlc]
STLCExtended.ty_arrow [constructor, in MoreStlc]
STLCExtended.ty_base [constructor, in MoreStlc]
STLCExtended.ty_list [constructor, in MoreStlc]
STLCExtended.ty_lookup [definition, in MoreStlc]
STLCExtended.ty_nat [constructor, in MoreStlc]
STLCExtended.ty_pair [constructor, in MoreStlc]
STLCExtended.ty_rcons [constructor, in MoreStlc]
STLCExtended.ty_rnil [constructor, in MoreStlc]
STLCExtended.T_Abs [constructor, in MoreStlc]
STLCExtended.T_App [constructor, in MoreStlc]
STLCExtended.T_Proj [constructor, in MoreStlc]
STLCExtended.T_RCons [constructor, in MoreStlc]
STLCExtended.T_RNil [constructor, in MoreStlc]
STLCExtended.T_Var [constructor, in MoreStlc]
STLCExtended.value [inductive, in MoreStlc]
STLCExtended.v_abs [constructor, in MoreStlc]
STLCExtended.v_rcons [constructor, in MoreStlc]
STLCExtended.v_rnil [constructor, in MoreStlc]
STLCExtended.weird_type [definition, in MoreStlc]
STLCExtended.well_formed_ty [inductive, in MoreStlc]
STLCExtended.wfty_arrow [constructor, in MoreStlc]
STLCExtended.wfty_base [constructor, in MoreStlc]
STLCExtended.wfty_list [constructor, in MoreStlc]
STLCExtended.wfty_nat [constructor, in MoreStlc]
STLCExtended.wfty_pair [constructor, in MoreStlc]
STLCExtended.wfty_rcons [constructor, in MoreStlc]
STLCExtended.wfty_rnil [constructor, in MoreStlc]
STLCExtended.wf_rcd_lookup [lemma, in MoreStlc]
STLC.a [abbreviation, in Stlc]
STLC.A [abbreviation, in Stlc]
STLC.afi_abs [constructor, in Stlc]
STLC.afi_app1 [constructor, in Stlc]
STLC.afi_app2 [constructor, in Stlc]
STLC.afi_var [constructor, in Stlc]
STLC.appears_free_in [inductive, in Stlc]
STLC.B [abbreviation, in Stlc]
STLC.b [abbreviation, in Stlc]
STLC.C [abbreviation, in Stlc]
STLC.c [abbreviation, in Stlc]
STLC.closed [definition, in Stlc]
STLC.context [definition, in Stlc]
STLC.context_invariance [lemma, in Stlc]
STLC.empty [definition, in Stlc]
STLC.extend [definition, in Stlc]
STLC.free_in_context [lemma, in Stlc]
STLC.has_type [inductive, in Stlc]
STLC.id_A [definition, in Stlc]
STLC.id_AarrowA [definition, in Stlc]
STLC.id_AarrowA_arrow_AarrowA [definition, in Stlc]
STLC.k [definition, in Stlc]
STLC.preservation [lemma, in Stlc]
STLC.progress [lemma, in Stlc]
STLC.progress' [lemma, in Stlc]
STLC.step [inductive, in Stlc]
STLC.stepmany [abbreviation, in Stlc]
STLC.step_example1 [lemma, in Stlc]
STLC.step_example2 [lemma, in Stlc]
STLC.step_example3 [lemma, in Stlc]
STLC.ST_AppAbs [constructor, in Stlc]
STLC.ST_App1 [constructor, in Stlc]
STLC.ST_App2 [constructor, in Stlc]
STLC.subst [definition, in Stlc]
STLC.substitution_preserves_typing [lemma, in Stlc]
STLC.tm [inductive, in Stlc]
STLC.tm_abs [constructor, in Stlc]
STLC.tm_app [constructor, in Stlc]
STLC.tm_var [constructor, in Stlc]
STLC.ty [inductive, in Stlc]
STLC.typable_empty__closed [lemma, in Stlc]
STLC.typing_example_1 [definition, in Stlc]
STLC.typing_example_1' [definition, in Stlc]
STLC.typing_example_2 [definition, in Stlc]
STLC.typing_example_2_full [definition, in Stlc]
STLC.typing_example_3 [definition, in Stlc]
STLC.typing_nonexample_1 [definition, in Stlc]
STLC.typing_nonexample_2 [definition, in Stlc]
STLC.typing_nonexample_3 [definition, in Stlc]
STLC.ty_arrow [constructor, in Stlc]
STLC.ty_base [constructor, in Stlc]
STLC.T_Abs [constructor, in Stlc]
STLC.T_App [constructor, in Stlc]
STLC.T_Var [constructor, in Stlc]
STLC.value [inductive, in Stlc]
STLC.v_abs [constructor, in Stlc]
stuck [definition, in Stlc]
ST_AppAbs [constructor, in Subtyping]
ST_App1 [constructor, in Subtyping]
ST_App2 [constructor, in Subtyping]
ST_If [constructor, in Stlc]
ST_IfFalse [constructor, in Stlc]
ST_IfTrue [constructor, in Stlc]
ST_Iszero [constructor, in Stlc]
ST_IszeroSucc [constructor, in Stlc]
ST_IszeroZero [constructor, in Stlc]
ST_PlusConstConst [constructor, in Smallstep]
ST_Plus1 [constructor, in Smallstep]
ST_Plus2 [constructor, in Smallstep]
ST_Pred [constructor, in Stlc]
ST_PredSucc [constructor, in Stlc]
ST_PredZero [constructor, in Stlc]
ST_ProjRcd [constructor, in Subtyping]
ST_Proj1 [constructor, in Subtyping]
ST_Rcd_Head [constructor, in Subtyping]
ST_Rcd_Tail [constructor, in Subtyping]
ST_Succ [constructor, in Stlc]
subst [definition, in Subtyping]
substitution_preserves_typing [lemma, in Subtyping]
subst_aexp [definition, in Equiv]
subst_aexp_ex [definition, in Equiv]
subst_equiv_property [definition, in Equiv]
subst_inequiv [lemma, in Equiv]
subst_inequiv' [lemma, in Equiv]
subtract_slowly [definition, in Imp]
subtract_slowly [definition, in Hoare]
subtract_slowly_body [definition, in Imp]
subtract_slowly_correct [lemma, in Hoare]
subtract_slowly_invariant [definition, in Hoare]
subtract_3_from_5_slowly [definition, in Imp]
subtype [inductive, in Subtyping]
subtype__wf [lemma, in Subtyping]
Subtyping [library]
sub_inversion_arrow [lemma, in Subtyping]
succ_hastype_nat__hastype_nat [definition, in Stlc]
sunday [constructor, in Basics]
swap_if_branches [lemma, in Equiv]
symmetric [definition, in Logic]
sym_aequiv [lemma, in Equiv]
sym_bequiv [lemma, in Equiv]
sym_cequiv [lemma, in Equiv]
sym_eq [lemma, in Poly]
S_Arrow [constructor, in Subtyping]
S_inj [lemma, in Poly]
S_le__S [lemma, in Hoare]
S_nbeq_0 [lemma, in Basics]
S_RcdDepth [constructor, in Subtyping]
S_RcdPerm [constructor, in Subtyping]
S_RcdWidth [constructor, in Subtyping]
S_Refl [constructor, in Subtyping]
S_Top [constructor, in Subtyping]
S_Trans [constructor, in Subtyping]
T
teen [definition, in Props]Temp1 [module, in Smallstep]
Temp1.step [inductive, in Smallstep]
Temp1.ST_PlusConstConst [constructor, in Smallstep]
Temp1.ST_Plus1 [constructor, in Smallstep]
Temp1.ST_Plus2 [constructor, in Smallstep]
Temp1.value [inductive, in Smallstep]
Temp1.value_not_same_as_normal_form [lemma, in Smallstep]
Temp1.v_const [constructor, in Smallstep]
Temp1.v_funny [constructor, in Smallstep]
Temp2 [module, in Smallstep]
Temp2.step [inductive, in Smallstep]
Temp2.ST_Funny [constructor, in Smallstep]
Temp2.ST_PlusConstConst [constructor, in Smallstep]
Temp2.ST_Plus1 [constructor, in Smallstep]
Temp2.ST_Plus2 [constructor, in Smallstep]
Temp2.value [inductive, in Smallstep]
Temp2.value_not_same_as_normal_form [lemma, in Smallstep]
Temp2.v_const [constructor, in Smallstep]
Temp3 [module, in Smallstep]
Temp3.step [inductive, in Smallstep]
Temp3.ST_PlusConstConst [constructor, in Smallstep]
Temp3.ST_Plus1 [constructor, in Smallstep]
Temp3.value [inductive, in Smallstep]
Temp3.value_not_same_as_normal_form [lemma, in Smallstep]
Temp3.v_const [constructor, in Smallstep]
Temp4 [module, in Smallstep]
Temp4.bool_step_prop1 [definition, in Smallstep]
Temp4.bool_step_prop2 [definition, in Smallstep]
Temp4.bool_step_prop3 [definition, in Smallstep]
Temp4.progress [lemma, in Smallstep]
Temp4.step [inductive, in Smallstep]
Temp4.step_deterministic [lemma, in Smallstep]
Temp4.ST_If [constructor, in Smallstep]
Temp4.ST_IfFalse [constructor, in Smallstep]
Temp4.ST_IfTrue [constructor, in Smallstep]
Temp4.Temp5.bool_step_prop4 [definition, in Smallstep]
Temp4.Temp5.bool_step_prop4_holds [definition, in Smallstep]
Temp4.Temp5.step [inductive, in Smallstep]
Temp4.Temp5.ST_If [constructor, in Smallstep]
Temp4.Temp5.ST_IfFalse [constructor, in Smallstep]
Temp4.Temp5.ST_IfTrue [constructor, in Smallstep]
Temp4.tm [inductive, in Smallstep]
Temp4.tm_false [constructor, in Smallstep]
Temp4.tm_if [constructor, in Smallstep]
Temp4.tm_true [constructor, in Smallstep]
Temp4.value [inductive, in Smallstep]
Temp4.v_false [constructor, in Smallstep]
Temp4.v_true [constructor, in Smallstep]
Temp5 [module, in Smallstep]
test_andb31 [definition, in Basics]
test_andb32 [definition, in Basics]
test_andb33 [definition, in Basics]
test_andb34 [definition, in Basics]
test_anon_fun [definition, in Poly]
test_anon_fun' [definition, in Poly]
test_ble_nat1 [definition, in Basics]
test_ble_nat2 [definition, in Basics]
test_ble_nat3 [definition, in Basics]
test_blt_nat1 [definition, in Basics]
test_blt_nat2 [definition, in Basics]
test_blt_nat3 [definition, in Basics]
test_countoddmembers'1 [definition, in Poly]
test_countoddmembers'2 [definition, in Poly]
test_countoddmembers'3 [definition, in Poly]
test_doit3times1 [definition, in Poly]
test_doit3times2 [definition, in Poly]
test_doit3times4 [definition, in Poly]
test_factorial1 [definition, in Basics]
test_factorial2 [definition, in Basics]
test_filter1 [definition, in Poly]
test_filter2 [definition, in Poly]
test_flat_map1 [definition, in Poly]
test_hd_opt1 [definition, in Poly]
test_hd_opt2 [definition, in Poly]
test_index1 [definition, in Poly]
test_index2 [definition, in Poly]
test_index3 [definition, in Poly]
test_length1 [definition, in Poly]
test_length2 [definition, in Poly]
test_le1 [lemma, in Logic]
test_le2 [lemma, in Logic]
test_le3 [lemma, in Logic]
test_map1 [definition, in Poly]
test_map2 [definition, in Poly]
test_map3 [definition, in Poly]
test_mult1 [definition, in Basics]
test_nandb1 [definition, in Basics]
test_nandb2 [definition, in Basics]
test_nandb3 [definition, in Basics]
test_nandb4 [definition, in Basics]
test_next_weekday [definition, in Basics]
test_oddb1 [definition, in Basics]
test_oddb2 [definition, in Basics]
test_orb1 [definition, in Basics]
test_orb2 [definition, in Basics]
test_orb3 [definition, in Basics]
test_orb4 [definition, in Basics]
test_plus3 [definition, in Poly]
test_plus3' [definition, in Poly]
test_plus3'' [definition, in Poly]
test_repeat1 [definition, in Poly]
test_rev1 [definition, in Poly]
test_rev2 [definition, in Poly]
test_stepmany_1 [lemma, in Smallstep]
test_stepmany_1' [lemma, in Smallstep]
test_stepmany_2 [lemma, in Smallstep]
test_stepmany_3 [lemma, in Smallstep]
test_stepmany_4 [lemma, in Smallstep]
thursday [constructor, in Basics]
tm [inductive, in Smallstep]
tm [inductive, in Subtyping]
tm [inductive, in Stlc]
tm_abs [constructor, in Subtyping]
tm_app [constructor, in Subtyping]
tm_const [constructor, in Smallstep]
tm_false [constructor, in Stlc]
tm_if [constructor, in Stlc]
tm_iszero [constructor, in Stlc]
tm_lookup [definition, in Subtyping]
tm_plus [constructor, in Smallstep]
tm_pred [constructor, in Stlc]
tm_proj [constructor, in Subtyping]
tm_rcons [constructor, in Subtyping]
tm_rnil [constructor, in Subtyping]
tm_succ [constructor, in Stlc]
tm_true [constructor, in Stlc]
tm_var [constructor, in Subtyping]
tm_zero [constructor, in Stlc]
transitive [definition, in Logic]
trans_aequiv [lemma, in Equiv]
trans_bequiv [lemma, in Equiv]
trans_cequiv [lemma, in Equiv]
trans_eq [lemma, in Poly]
trans_eq_example [definition, in Poly]
trans_eq_example' [definition, in Poly]
trans_eq_exercise [definition, in Poly]
tree [inductive, in Props]
true [constructor, in Basics]
true_for_all_numbers [definition, in Props]
true_for_n__true_for_Sn [definition, in Props]
true_for_zero [definition, in Props]
tuesday [constructor, in Basics]
ty [inductive, in Stlc]
ty [inductive, in Subtyping]
typing_inversion_abs [lemma, in Subtyping]
typing_inversion_app [lemma, in Subtyping]
typing_inversion_proj [lemma, in Subtyping]
typing_inversion_rcons [lemma, in Subtyping]
typing_inversion_var [lemma, in Subtyping]
ty_arrow [constructor, in Subtyping]
ty_base [constructor, in Subtyping]
ty_bool [constructor, in Stlc]
ty_lookup [definition, in Subtyping]
ty_nat [constructor, in Stlc]
ty_rcons [constructor, in Subtyping]
ty_rnil [constructor, in Subtyping]
ty_top [constructor, in Subtyping]
T_Abs [constructor, in Subtyping]
T_App [constructor, in Subtyping]
T_False [constructor, in Stlc]
T_If [constructor, in Stlc]
T_Iszero [constructor, in Stlc]
T_Pred [constructor, in Stlc]
T_Proj [constructor, in Subtyping]
T_RCons [constructor, in Subtyping]
T_RNil [constructor, in Subtyping]
T_Sub [constructor, in Subtyping]
T_Succ [constructor, in Stlc]
T_True [constructor, in Stlc]
T_Var [constructor, in Subtyping]
T_Zero [constructor, in Stlc]
U
uncurry_curry [lemma, in Poly]unfold_example [lemma, in Poly]
V
value [inductive, in Subtyping]value [definition, in Stlc]
value [inductive, in Smallstep]
value_is_nf [lemma, in Smallstep]
value_is_nf [lemma, in Stlc]
v_abs [constructor, in Subtyping]
v_const [constructor, in Smallstep]
v_rcons [constructor, in Subtyping]
v_rnil [constructor, in Subtyping]
W
wednesday [constructor, in Basics]well_formed_ty [inductive, in Subtyping]
wfty_arrow [constructor, in Subtyping]
wfty_base [constructor, in Subtyping]
wfty_rcons [constructor, in Subtyping]
wfty_rnil [constructor, in Subtyping]
wfty_top [constructor, in Subtyping]
wf_rcd_lookup [lemma, in Subtyping]
X
X [definition, in Imp]XtimesYinZ [definition, in Imp]
Y
Y [definition, in Imp]yes [constructor, in Props]
yesno [inductive, in Props]
Z
Z [definition, in Imp]zero_nbeq_plus_1 [lemma, in Basics]
zero_nbeq_S [lemma, in Basics]
Lemma Index
A
abs_arrow [in Subtyping]aequiv_example [in Equiv]
AExp.foo [in Imp]
AExp.foo' [in Imp]
AExp.foo'' [in Imp]
AExp.optimize_0plus_sound [in Imp]
AExp.optimize_0plus_sound' [in Imp]
AExp.optimize_0plus_sound'' [in Imp]
all3_spec [in Basics]
andb_false [in Logic]
andb_false_r [in Basics]
andb_true [in Logic]
andb_true [in SfLib]
andb_true_elim1 [in SfLib]
andb_true_elim1 [in Basics]
andb_true_elim2 [in SfLib]
andb_true_elim2 [in Basics]
and_assoc [in Logic]
and_commut [in Logic]
and_example [in Logic]
and_example' [in Logic]
auto_example_1 [in Stlc]
auto_example_2 [in Stlc]
auto_example_3 [in Stlc]
B
bequiv_example [in Equiv]beq_false_not_eq [in Logic]
beq_id_eq [in Imp]
beq_id_false_not_eq [in Imp]
beq_id_refl [in Imp]
beq_nat_eq [in Poly]
beq_nat_eq' [in Poly]
beq_nat_refl [in Basics]
beq_nat_trans [in Poly]
beq_nat_0_l [in Poly]
beq_nat_0_r [in Poly]
bexp_eval_false [in Hoare]
bexp_eval_true [in Hoare]
ble_nat_false [in Logic]
ble_nat_false [in SfLib]
ble_nat_n_Sn_false [in Logic]
ble_nat_refl [in Basics]
ble_nat_true [in Logic]
ble_nat_true [in SfLib]
C
canonical_forms_of_arrow_types [in Subtyping]CAss_congruence [in Equiv]
cequiv_state [in Equiv]
ceval_and_ceval_step_coincide [in Imp]
ceval_deterministic [in Equiv]
ceval_deterministic' [in Equiv]
ceval_step_more [in Imp]
ceval_step__ceval [in Imp]
ceval__ceval_step [in Imp]
CIf_congruence [in Equiv]
CIf_false [in Equiv]
CIf_true [in Equiv]
CIf_true_simple [in Equiv]
context_invariance [in Subtyping]
contradiction_implies_anything [in Logic]
contrapositive [in Logic]
CSeq_congruence [in Equiv]
curry_uncurry [in Poly]
CWhile_congruence [in Equiv]
CWhile_false [in Equiv]
CWhile_true [in Equiv]
CWhile_true_nonterm [in Equiv]
D
dist_exists_or [in Logic]dist_not_exists [in Logic]
double_even [in Props]
double_injective [in Poly]
double_injective' [in Props]
double_injective_FAILED [in Props]
double_injective_take2 [in Props]
double_injective_take2_FAILED [in Props]
double_neg [in Logic]
E
eqnat_false_S [in Props]eq_add_S [in Poly]
eval__stepmany [in Smallstep]
eval__value [in Smallstep]
evenb_n__oddb_Sn [in Basics]
even5_nonsense [in Props]
even_ev [in Logic]
ev_even [in Props]
ev_even' [in Props]
ev_ev_even [in Props]
ev_minus2 [in Props]
ev_minus2' [in Props]
ev_MyProp [in Props]
ev_MyProp' [in Props]
ev_not_ev_S [in Logic]
ev_not_ev_S [in SfLib]
ev_plus4' [in Props]
ev_sum [in Props]
exists_example_2 [in Logic]
ex_falso_quodlibet [in SfLib]
ex_falso_quodlibet [in Logic]
F
Factorial.fact_com_correct [in Hoare]fact_body_preserves_invariant [in Equiv]
fact_com_correct [in Equiv]
fact_loop_preserves_invariant [in Equiv]
failed_proof [in Props]
False_implies_nonsense [in Logic]
filter_exercise [in Poly]
find_parity_correct [in Hoare]
five_not_even [in Logic]
fold_constants_aexp_sound [in Equiv]
fold_constants_aexp_sound' [in Equiv]
fold_constants_bexp_sound [in Equiv]
fold_constants_com_sound [in Equiv]
four_ev' [in Props]
free_in_context [in Subtyping]
G
guard_false_after_loop [in Equiv]H
has_type__wf [in Subtyping]hoare_asgn [in Hoare]
hoare_asgn_eq [in Hoare]
hoare_consequence [in Hoare]
hoare_consequence_post [in Hoare]
hoare_consequence_pre [in Hoare]
hoare_if [in Hoare]
hoare_post_true [in Hoare]
hoare_pre_false [in Hoare]
hoare_seq [in Hoare]
hoare_skip [in Hoare]
hoare_while [in Hoare]
I
iff_implies [in Logic]iff_refl [in Logic]
iff_sym [in Logic]
iff_trans [in Logic]
iff_trans [in Equiv]
index_after_last [in Props]
inequiv_exercise [in Equiv]
L
length_appendtwice [in Props]length_append_cons [in Props]
length_snoc' [in Poly]
length_snoc'' [in Poly]
length_snoc''' [in Props]
le_antisymmetric [in Logic]
le_not_a_partial_function [in Logic]
le_not_symmetric [in Logic]
le_order [in Logic]
le_plus_l [in Logic]
le_reflexive [in Logic]
le_Sn_le [in Logic]
le_Sn_n [in Logic]
le_step [in Logic]
le_S_n [in Logic]
le_trans [in Logic]
lookup_field_in_value [in Subtyping]
loop_never_stops [in Imp]
loop_unrolling [in Equiv]
lt_S [in Logic]
lt_trans [in Logic]
lt_trans' [in Logic]
lt_trans'' [in Logic]
M
map_rev [in Poly]minus_diag [in Basics]
minus_pred [in Hoare]
minus_0_n [in Hoare]
mult_assoc [in Basics]
mult_comm [in Basics]
mult_plus_distr_r [in Basics]
mult_0_l [in Basics]
mult_0_plus [in Basics]
mult_0_plus' [in Basics]
mult_0_r [in Basics]
mult_0_r' [in Props]
mult_0_r'' [in Props]
mult_1_l [in Basics]
mult_1_plus [in Basics]
MyEquality.two_defs_of_eq_coincide [in Logic]
MyProp_ev [in Props]
MyProp_plustwo [in Props]
MyProp_ten [in Props]
MyProp_0 [in Props]
N
NatList.append_snoc [in Lists]NatList.app_length [in Lists]
NatList.app_nil_end [in Lists]
NatList.ass_app [in Lists]
NatList.ass_app' [in Lists]
NatList.ass_app4 [in Lists]
NatList.beq_natlist_refl [in Lists]
NatList.beq_nat_sym [in Lists]
NatList.ble_n_Sn [in Lists]
NatList.count_member_nonzero [in Lists]
NatList.distr_rev [in Lists]
NatList.fst_swap_is_snd [in Lists]
NatList.length_snoc [in Lists]
NatList.nil_app [in Lists]
NatList.nonzeros_length [in Lists]
NatList.option_elim_hd [in Lists]
NatList.remove_decreases_count [in Lists]
NatList.rev_exercise1 [in Lists]
NatList.rev_involutive [in Lists]
NatList.rev_length [in Lists]
NatList.rev_length_firsttry [in Lists]
NatList.silly1 [in Lists]
NatList.silly2 [in Lists]
NatList.silly2a [in Lists]
NatList.silly3 [in Lists]
NatList.silly3_firsttry [in Lists]
NatList.silly_ex [in Lists]
NatList.snd_fst_is_swap [in Lists]
NatList.snoc_append [in Lists]
NatList.surjective_pairing [in Lists]
NatList.surjective_pairing' [in Lists]
NatList.surjective_pairing_stuck [in Lists]
NatList.sym_eq_bool [in Lists]
NatList.tl_length_pred [in Lists]
negb_involutive [in Basics]
neq0_not_true__eq_0 [in Hoare]
neq0_true__eq_S [in Hoare]
next_nat_closure_is_le [in Smallstep]
next_nat_partial_function [in Logic]
nf_is_value [in Smallstep]
nil_app [in Poly]
nonsense_implies_False [in Logic]
normal_forms_unique [in Smallstep]
not_both_true_and_false [in Logic]
not_eq_beq_false [in SfLib]
not_eq_beq_false [in Logic]
not_eq_beq_id_false [in Imp]
not_ev_ev_S [in Hoare]
not_ev_ev_S_gen [in Hoare]
not_False [in Logic]
not_false_then_true [in Logic]
no_whiles_eqv [in Imp]
n_le_m__Sn_le_Sm [in Logic]
O
orb_false [in Logic]orb_true [in Logic]
or_commut [in Logic]
or_commut' [in Logic]
or_distributes_over_and [in Logic]
or_distributes_over_and_1 [in Logic]
or_distributes_over_and_2 [in Logic]
our_nat_induction_works [in Props]
our_nat_induction_works' [in Props]
override_eq [in Imp]
override_eq [in Poly]
override_example [in Imp]
override_example [in Poly]
override_neq [in Imp]
override_neq [in Poly]
override_permute [in Poly]
override_permute [in Imp]
override_same [in Imp]
override_same [in Poly]
override_shadow [in Poly]
override_shadow [in Imp]
O_le_n [in Logic]
P
plus2_spec [in Imp]plus_assoc [in Basics]
plus_assoc' [in Props]
plus_assoc' [in Basics]
plus_ble_compat_l [in Basics]
plus_comm [in Basics]
plus_comm' [in Props]
plus_comm'' [in Props]
plus_fact_is_true [in Props]
plus_id_example [in Basics]
plus_id_exercise [in Basics]
plus_lt [in Logic]
plus_n_n_injective [in Poly]
plus_n_n_injective_take2 [in Props]
plus_n_Sm [in Basics]
plus_one_r' [in Props]
plus_one_r'' [in Props]
plus_O_n [in Basics]
plus_O_n' [in Basics]
plus_O_n'' [in Basics]
plus_rearrange_firsttry [in Basics]
plus_swap [in Basics]
plus_swap' [in Basics]
plus_0_r [in Basics]
plus_0_r_firsttry [in Basics]
plus_0_r_secondtry [in Basics]
plus_1_l [in Basics]
plus_1_neq_0 [in Basics]
plus_1_neq_0_firsttry [in Basics]
plus_2_2_is_4 [in Props]
preservation [in Stlc]
preservation [in Subtyping]
preservation' [in Stlc]
progress [in Stlc]
progress [in Smallstep]
progress [in Subtyping]
proj1 [in Logic]
proj2 [in Logic]
R
random_fact_1 [in Hoare]random_fact_2 [in Hoare]
rcd_types_match [in Subtyping]
reduce_to_zero_correct [in Hoare]
refl_aequiv [in Equiv]
refl_bequiv [in Equiv]
refl_cequiv [in Equiv]
rev_snoc [in Poly]
rsc_R [in Smallstep]
rsc_trans [in Smallstep]
rtc_rsc_coincide [in Smallstep]
S
seq_assoc [in Equiv]sillyfun1_odd [in Poly]
sillyfun1_odd_FAILED [in Poly]
sillyfun_false [in Poly]
silly3' [in Poly]
silly4 [in Poly]
silly5 [in Poly]
silly6 [in Poly]
silly7 [in Poly]
SimpleArith2.step_deterministic [in Smallstep]
skip_left [in Equiv]
skip_right [in Equiv]
snoc_with_append [in Poly]
soundness [in Stlc]
sqrt_com_correct [in Hoare]
SSev_even [in Props]
SSev_ev_firsttry [in Props]
SSSSev_even [in Props]
stepmany_congr_1 [in Smallstep]
stepmany_congr_2 [in Smallstep]
stepmany_iff_eval [in Smallstep]
stepmany__eval [in Smallstep]
step_deterministic [in Smallstep]
step_deterministic [in Stlc]
step_normalizing [in Smallstep]
step_preserves_record_tm [in Subtyping]
step__eval [in Smallstep]
STLCChecker.beq_ty_refl [in MoreStlc]
STLCChecker.beq_ty__eq [in MoreStlc]
STLCChecker.type_checking_complete [in MoreStlc]
STLCChecker.type_checking_sound [in MoreStlc]
STLCExtended.context_invariance [in MoreStlc]
STLCExtended.free_in_context [in MoreStlc]
STLCExtended.has_type__wf [in MoreStlc]
STLCExtended.lookup_field_in_value [in MoreStlc]
STLCExtended.preservation [in MoreStlc]
STLCExtended.progress [in MoreStlc]
STLCExtended.step_preserves_record_tm [in MoreStlc]
STLCExtended.substitution_preserves_typing [in MoreStlc]
STLCExtended.typing_example_2 [in MoreStlc]
STLCExtended.wf_rcd_lookup [in MoreStlc]
STLC.context_invariance [in Stlc]
STLC.free_in_context [in Stlc]
STLC.preservation [in Stlc]
STLC.progress [in Stlc]
STLC.progress' [in Stlc]
STLC.step_example1 [in Stlc]
STLC.step_example2 [in Stlc]
STLC.step_example3 [in Stlc]
STLC.substitution_preserves_typing [in Stlc]
STLC.typable_empty__closed [in Stlc]
substitution_preserves_typing [in Subtyping]
subst_inequiv [in Equiv]
subst_inequiv' [in Equiv]
subtract_slowly_correct [in Hoare]
subtype__wf [in Subtyping]
sub_inversion_arrow [in Subtyping]
swap_if_branches [in Equiv]
sym_aequiv [in Equiv]
sym_bequiv [in Equiv]
sym_cequiv [in Equiv]
sym_eq [in Poly]
S_inj [in Poly]
S_le__S [in Hoare]
S_nbeq_0 [in Basics]
T
Temp1.value_not_same_as_normal_form [in Smallstep]Temp2.value_not_same_as_normal_form [in Smallstep]
Temp3.value_not_same_as_normal_form [in Smallstep]
Temp4.progress [in Smallstep]
Temp4.step_deterministic [in Smallstep]
test_le1 [in Logic]
test_le2 [in Logic]
test_le3 [in Logic]
test_stepmany_1 [in Smallstep]
test_stepmany_1' [in Smallstep]
test_stepmany_2 [in Smallstep]
test_stepmany_3 [in Smallstep]
test_stepmany_4 [in Smallstep]
trans_aequiv [in Equiv]
trans_bequiv [in Equiv]
trans_cequiv [in Equiv]
trans_eq [in Poly]
typing_inversion_abs [in Subtyping]
typing_inversion_app [in Subtyping]
typing_inversion_proj [in Subtyping]
typing_inversion_rcons [in Subtyping]
typing_inversion_var [in Subtyping]
U
uncurry_curry [in Poly]unfold_example [in Poly]
V
value_is_nf [in Smallstep]value_is_nf [in Stlc]
W
wf_rcd_lookup [in Subtyping]Z
zero_nbeq_plus_1 [in Basics]zero_nbeq_S [in Basics]
Constructor Index
A
AExp.AMinus [in Imp]AExp.AMult [in Imp]
AExp.ANum [in Imp]
AExp.APlus [in Imp]
AExp.BAnd [in Imp]
AExp.BEq [in Imp]
AExp.BFalse [in Imp]
AExp.BLe [in Imp]
AExp.BNot [in Imp]
AExp.BOr [in Imp]
AExp.BTrue [in Imp]
afi_abs [in Subtyping]
afi_app1 [in Subtyping]
afi_app2 [in Subtyping]
afi_proj [in Subtyping]
afi_rhead [in Subtyping]
afi_rtail [in Subtyping]
afi_var [in Subtyping]
AId [in Imp]
AMinus [in Imp]
AMult [in Imp]
ANum [in Imp]
APlus [in Imp]
B
BAnd [in Imp]BEq [in Imp]
BFalse [in Imp]
BLe [in Imp]
blue [in Props]
BNot [in Imp]
bool_cons [in Poly]
bool_nil [in Poly]
BOr [in Imp]
BTrue [in Imp]
bv_false [in Stlc]
bv_true [in Stlc]
C
CAss [in Imp]CEAss [in Imp]
CEIfFalse [in Imp]
CEIfTrue [in Imp]
CESeq [in Imp]
CESkip [in Imp]
CEWhileEnd [in Imp]
CEWhileLoop [in Imp]
CIf [in Imp]
Combined.ST_If [in Smallstep]
Combined.ST_IfFalse [in Smallstep]
Combined.ST_IfTrue [in Smallstep]
Combined.ST_PlusConstConst [in Smallstep]
Combined.ST_Plus1 [in Smallstep]
Combined.ST_Plus2 [in Smallstep]
Combined.tm_const [in Smallstep]
Combined.tm_false [in Smallstep]
Combined.tm_if [in Smallstep]
Combined.tm_plus [in Smallstep]
Combined.tm_true [in Smallstep]
Combined.v_const [in Smallstep]
Combined.v_false [in Smallstep]
Combined.v_true [in Smallstep]
conj [in Logic]
cons [in Poly]
CSeq [in Imp]
CSkip [in Imp]
CWhile [in Imp]
C1 [in Props]
C2 [in Props]
E
ev_SS [in Props]ev_SS [in SfLib]
ev_0 [in Props]
ev_0 [in SfLib]
Excerpt_From_Coq_Relations_Library.rt_refl [in Smallstep]
Excerpt_From_Coq_Relations_Library.rt_step [in Smallstep]
Excerpt_From_Coq_Relations_Library.rt_trans [in Smallstep]
ex_intro [in Logic]
E_Const [in Smallstep]
E_Plus [in Smallstep]
F
false [in Basics]FirstLe.le_n [in Logic]
FirstLe.le_S [in Logic]
friday [in Basics]
G
green [in Props]I
Id [in Imp]L
leaf [in Props]le_n [in Logic]
le_S [in Logic]
M
monday [in Basics]MumbleBaz.a [in Poly]
MumbleBaz.b [in Poly]
MumbleBaz.c [in Poly]
MumbleBaz.d [in Poly]
MumbleBaz.e [in Poly]
MumbleBaz.x [in Poly]
MumbleBaz.y [in Poly]
MyEquality.refl_equal [in Logic]
MyEquality.refl_equal' [in Logic]
MyProp1 [in Props]
MyProp2 [in Props]
MyProp3 [in Props]
N
NatList.cons [in Lists]NatList.nil [in Lists]
NatList.None [in Lists]
NatList.pair [in Lists]
NatList.Some [in Lists]
ncons [in Props]
ne_1 [in Logic]
ne_2 [in Logic]
nil [in Poly]
nn [in Logic]
nn [in Smallstep]
nnil [in Props]
nnil1 [in Props]
no [in Props]
node [in Props]
None [in Poly]
nsnoc1 [in Props]
nv_succ [in Stlc]
nv_zero [in Stlc]
O
or_introl [in Logic]or_intror [in Logic]
P
pair [in Poly]Playground1.O [in Basics]
Playground1.S [in Basics]
P.c1 [in Props]
P.c2 [in Props]
P.c3 [in Props]
R
red [in Props]RepeatExercise.CAss [in Hoare]
RepeatExercise.CEAss [in Hoare]
RepeatExercise.CEIfFalse [in Hoare]
RepeatExercise.CEIfTrue [in Hoare]
RepeatExercise.CESeq [in Hoare]
RepeatExercise.CESkip [in Hoare]
RepeatExercise.CEWhileEnd [in Hoare]
RepeatExercise.CEWhileLoop [in Hoare]
RepeatExercise.CIf [in Hoare]
RepeatExercise.CRepeat [in Hoare]
RepeatExercise.CSeq [in Hoare]
RepeatExercise.CSkip [in Hoare]
RepeatExercise.CWhile [in Hoare]
rsc_refl [in Smallstep]
rsc_step [in Smallstep]
rtm_cons [in Subtyping]
rtm_nil [in Subtyping]
rty_cons [in Subtyping]
rty_nil [in Subtyping]
R.c1 [in Logic]
R.c2 [in Logic]
R.c3 [in Logic]
R.c4 [in Logic]
R.c5 [in Logic]
S
saturday [in Basics]SimpleArith1.E_Const [in Smallstep]
SimpleArith1.E_Plus [in Smallstep]
SimpleArith2.ST_PlusConstConst [in Smallstep]
SimpleArith2.ST_Plus1 [in Smallstep]
SimpleArith2.ST_Plus2 [in Smallstep]
Some [in Poly]
sq [in Logic]
STLCArith.tm_abs [in Stlc]
STLCArith.tm_app [in Stlc]
STLCArith.tm_if0 [in Stlc]
STLCArith.tm_mult [in Stlc]
STLCArith.tm_nat [in Stlc]
STLCArith.tm_pred [in Stlc]
STLCArith.tm_succ [in Stlc]
STLCArith.tm_var [in Stlc]
STLCArith.ty_arrow [in Stlc]
STLCArith.ty_nat [in Stlc]
STLCExtended.afi_abs [in MoreStlc]
STLCExtended.afi_app1 [in MoreStlc]
STLCExtended.afi_app2 [in MoreStlc]
STLCExtended.afi_proj [in MoreStlc]
STLCExtended.afi_rhead [in MoreStlc]
STLCExtended.afi_rtail [in MoreStlc]
STLCExtended.afi_var [in MoreStlc]
STLCExtended.FirstTry.ty_arrow [in MoreStlc]
STLCExtended.FirstTry.ty_base [in MoreStlc]
STLCExtended.FirstTry.ty_rcd [in MoreStlc]
STLCExtended.rtm_cons [in MoreStlc]
STLCExtended.rtm_nil [in MoreStlc]
STLCExtended.rty_cons [in MoreStlc]
STLCExtended.rty_nil [in MoreStlc]
STLCExtended.ST_AppAbs [in MoreStlc]
STLCExtended.ST_App1 [in MoreStlc]
STLCExtended.ST_App2 [in MoreStlc]
STLCExtended.ST_ProjRcd [in MoreStlc]
STLCExtended.ST_Proj1 [in MoreStlc]
STLCExtended.ST_Rcd_Head [in MoreStlc]
STLCExtended.ST_Rcd_Tail [in MoreStlc]
STLCExtended.tm_abs [in MoreStlc]
STLCExtended.tm_app [in MoreStlc]
STLCExtended.tm_case [in MoreStlc]
STLCExtended.tm_cons [in MoreStlc]
STLCExtended.tm_fix [in MoreStlc]
STLCExtended.tm_fst [in MoreStlc]
STLCExtended.tm_if0 [in MoreStlc]
STLCExtended.tm_let [in MoreStlc]
STLCExtended.tm_mult [in MoreStlc]
STLCExtended.tm_nat [in MoreStlc]
STLCExtended.tm_nil [in MoreStlc]
STLCExtended.tm_pair [in MoreStlc]
STLCExtended.tm_pred [in MoreStlc]
STLCExtended.tm_proj [in MoreStlc]
STLCExtended.tm_rcons [in MoreStlc]
STLCExtended.tm_rnil [in MoreStlc]
STLCExtended.tm_snd [in MoreStlc]
STLCExtended.tm_succ [in MoreStlc]
STLCExtended.tm_var [in MoreStlc]
STLCExtended.ty_arrow [in MoreStlc]
STLCExtended.ty_base [in MoreStlc]
STLCExtended.ty_list [in MoreStlc]
STLCExtended.ty_nat [in MoreStlc]
STLCExtended.ty_pair [in MoreStlc]
STLCExtended.ty_rcons [in MoreStlc]
STLCExtended.ty_rnil [in MoreStlc]
STLCExtended.T_Abs [in MoreStlc]
STLCExtended.T_App [in MoreStlc]
STLCExtended.T_Proj [in MoreStlc]
STLCExtended.T_RCons [in MoreStlc]
STLCExtended.T_RNil [in MoreStlc]
STLCExtended.T_Var [in MoreStlc]
STLCExtended.v_abs [in MoreStlc]
STLCExtended.v_rcons [in MoreStlc]
STLCExtended.v_rnil [in MoreStlc]
STLCExtended.wfty_arrow [in MoreStlc]
STLCExtended.wfty_base [in MoreStlc]
STLCExtended.wfty_list [in MoreStlc]
STLCExtended.wfty_nat [in MoreStlc]
STLCExtended.wfty_pair [in MoreStlc]
STLCExtended.wfty_rcons [in MoreStlc]
STLCExtended.wfty_rnil [in MoreStlc]
STLC.afi_abs [in Stlc]
STLC.afi_app1 [in Stlc]
STLC.afi_app2 [in Stlc]
STLC.afi_var [in Stlc]
STLC.ST_AppAbs [in Stlc]
STLC.ST_App1 [in Stlc]
STLC.ST_App2 [in Stlc]
STLC.tm_abs [in Stlc]
STLC.tm_app [in Stlc]
STLC.tm_var [in Stlc]
STLC.ty_arrow [in Stlc]
STLC.ty_base [in Stlc]
STLC.T_Abs [in Stlc]
STLC.T_App [in Stlc]
STLC.T_Var [in Stlc]
STLC.v_abs [in Stlc]
ST_AppAbs [in Subtyping]
ST_App1 [in Subtyping]
ST_App2 [in Subtyping]
ST_If [in Stlc]
ST_IfFalse [in Stlc]
ST_IfTrue [in Stlc]
ST_Iszero [in Stlc]
ST_IszeroSucc [in Stlc]
ST_IszeroZero [in Stlc]
ST_PlusConstConst [in Smallstep]
ST_Plus1 [in Smallstep]
ST_Plus2 [in Smallstep]
ST_Pred [in Stlc]
ST_PredSucc [in Stlc]
ST_PredZero [in Stlc]
ST_ProjRcd [in Subtyping]
ST_Proj1 [in Subtyping]
ST_Rcd_Head [in Subtyping]
ST_Rcd_Tail [in Subtyping]
ST_Succ [in Stlc]
sunday [in Basics]
S_Arrow [in Subtyping]
S_RcdDepth [in Subtyping]
S_RcdPerm [in Subtyping]
S_RcdWidth [in Subtyping]
S_Refl [in Subtyping]
S_Top [in Subtyping]
S_Trans [in Subtyping]
T
Temp1.ST_PlusConstConst [in Smallstep]Temp1.ST_Plus1 [in Smallstep]
Temp1.ST_Plus2 [in Smallstep]
Temp1.v_const [in Smallstep]
Temp1.v_funny [in Smallstep]
Temp2.ST_Funny [in Smallstep]
Temp2.ST_PlusConstConst [in Smallstep]
Temp2.ST_Plus1 [in Smallstep]
Temp2.ST_Plus2 [in Smallstep]
Temp2.v_const [in Smallstep]
Temp3.ST_PlusConstConst [in Smallstep]
Temp3.ST_Plus1 [in Smallstep]
Temp3.v_const [in Smallstep]
Temp4.ST_If [in Smallstep]
Temp4.ST_IfFalse [in Smallstep]
Temp4.ST_IfTrue [in Smallstep]
Temp4.Temp5.ST_If [in Smallstep]
Temp4.Temp5.ST_IfFalse [in Smallstep]
Temp4.Temp5.ST_IfTrue [in Smallstep]
Temp4.tm_false [in Smallstep]
Temp4.tm_if [in Smallstep]
Temp4.tm_true [in Smallstep]
Temp4.v_false [in Smallstep]
Temp4.v_true [in Smallstep]
thursday [in Basics]
tm_abs [in Subtyping]
tm_app [in Subtyping]
tm_const [in Smallstep]
tm_false [in Stlc]
tm_if [in Stlc]
tm_iszero [in Stlc]
tm_plus [in Smallstep]
tm_pred [in Stlc]
tm_proj [in Subtyping]
tm_rcons [in Subtyping]
tm_rnil [in Subtyping]
tm_succ [in Stlc]
tm_true [in Stlc]
tm_var [in Subtyping]
tm_zero [in Stlc]
true [in Basics]
tuesday [in Basics]
ty_arrow [in Subtyping]
ty_base [in Subtyping]
ty_bool [in Stlc]
ty_nat [in Stlc]
ty_rcons [in Subtyping]
ty_rnil [in Subtyping]
ty_top [in Subtyping]
T_Abs [in Subtyping]
T_App [in Subtyping]
T_False [in Stlc]
T_If [in Stlc]
T_Iszero [in Stlc]
T_Pred [in Stlc]
T_Proj [in Subtyping]
T_RCons [in Subtyping]
T_RNil [in Subtyping]
T_Sub [in Subtyping]
T_Succ [in Stlc]
T_True [in Stlc]
T_Var [in Subtyping]
T_Zero [in Stlc]
V
v_abs [in Subtyping]v_const [in Smallstep]
v_rcons [in Subtyping]
v_rnil [in Subtyping]
W
wednesday [in Basics]wfty_arrow [in Subtyping]
wfty_base [in Subtyping]
wfty_rcons [in Subtyping]
wfty_rnil [in Subtyping]
wfty_top [in Subtyping]
Y
yes [in Props]Inductive Index
A
aexp [in Imp]AExp.aexp [in Imp]
AExp.bexp [in Imp]
and [in Logic]
appears_free_in [in Subtyping]
B
bexp [in Imp]bool [in Basics]
boollist [in Poly]
bvalue [in Stlc]
C
ceval [in Imp]com [in Imp]
Combined.step [in Smallstep]
Combined.tm [in Smallstep]
Combined.value [in Smallstep]
D
day [in Basics]E
ev [in Props]ev [in SfLib]
eval [in Smallstep]
ex [in Logic]
Excerpt_From_Coq_Relations_Library.clos_refl_trans [in Smallstep]
F
False [in Logic]FirstLe.le [in Logic]
foo' [in Props]
H
has_type [in Subtyping]has_type [in Stlc]
I
id [in Imp]L
le [in Logic]list [in Poly]
M
MumbleBaz.baz [in Poly]MumbleBaz.grumble [in Poly]
MumbleBaz.mumble [in Poly]
MyEquality.eq [in Logic]
MyEquality.eq' [in Logic]
MyProp [in Props]
N
natlist [in Props]NatList.natlist [in Lists]
NatList.natoption [in Lists]
NatList.natprod [in Lists]
natlist1 [in Props]
next_even [in Logic]
next_nat [in Smallstep]
next_nat [in Logic]
no_Whiles [in Imp]
nvalue [in Stlc]
O
option [in Poly]or [in Logic]
P
Playground1.nat [in Basics]prod [in Poly]
P.p [in Props]
R
record_tm [in Subtyping]record_ty [in Subtyping]
refl_step_closure [in Smallstep]
RepeatExercise.ceval [in Hoare]
RepeatExercise.com [in Hoare]
rgb [in Props]
R.R [in Logic]
S
SimpleArith1.eval [in Smallstep]SimpleArith2.step [in Smallstep]
square_of [in Logic]
step [in Smallstep]
step [in Subtyping]
step [in Stlc]
STLCArith.tm [in Stlc]
STLCArith.ty [in Stlc]
STLCExtended.appears_free_in [in MoreStlc]
STLCExtended.FirstTry.ty [in MoreStlc]
STLCExtended.has_type [in MoreStlc]
STLCExtended.record_tm [in MoreStlc]
STLCExtended.record_ty [in MoreStlc]
STLCExtended.step [in MoreStlc]
STLCExtended.tm [in MoreStlc]
STLCExtended.ty [in MoreStlc]
STLCExtended.value [in MoreStlc]
STLCExtended.well_formed_ty [in MoreStlc]
STLC.appears_free_in [in Stlc]
STLC.has_type [in Stlc]
STLC.step [in Stlc]
STLC.tm [in Stlc]
STLC.ty [in Stlc]
STLC.value [in Stlc]
subtype [in Subtyping]
T
Temp1.step [in Smallstep]Temp1.value [in Smallstep]
Temp2.step [in Smallstep]
Temp2.value [in Smallstep]
Temp3.step [in Smallstep]
Temp3.value [in Smallstep]
Temp4.step [in Smallstep]
Temp4.Temp5.step [in Smallstep]
Temp4.tm [in Smallstep]
Temp4.value [in Smallstep]
tm [in Smallstep]
tm [in Subtyping]
tm [in Stlc]
tree [in Props]
ty [in Stlc]
ty [in Subtyping]
V
value [in Subtyping]value [in Smallstep]
W
well_formed_ty [in Subtyping]Y
yesno [in Props]Abbreviation Index
A
AExp.A0 [in Imp]AExp.A1 [in Imp]
AExp.A2 [in Imp]
AExp.A3 [in Imp]
AExp.A4 [in Imp]
AExp.A5 [in Imp]
A0 [in Imp]
A1 [in Imp]
A2 [in Imp]
A3 [in Imp]
A4 [in Imp]
A5 [in Imp]
A6 [in Imp]
E
Examples.A [in Subtyping]Examples.B [in Subtyping]
Examples.C [in Subtyping]
Examples.i [in Subtyping]
Examples.j [in Subtyping]
Examples.k [in Subtyping]
Examples.x [in Subtyping]
Examples.y [in Subtyping]
Examples.z [in Subtyping]
S
stepmany [in Smallstep]step_normal_form [in Stlc]
step_normal_form [in Smallstep]
STLCExtended.a [in MoreStlc]
STLCExtended.A [in MoreStlc]
STLCExtended.B [in MoreStlc]
STLCExtended.f [in MoreStlc]
STLCExtended.g [in MoreStlc]
STLCExtended.i1 [in MoreStlc]
STLCExtended.i2 [in MoreStlc]
STLCExtended.k [in MoreStlc]
STLCExtended.l [in MoreStlc]
STLCExtended.stepmany [in MoreStlc]
STLC.a [in Stlc]
STLC.A [in Stlc]
STLC.B [in Stlc]
STLC.b [in Stlc]
STLC.C [in Stlc]
STLC.c [in Stlc]
STLC.stepmany [in Stlc]
Definition Index
A
add_slowly [in Hoare]admit [in Basics]
aequiv [in Equiv]
aeval [in Imp]
AExp.aeval [in Imp]
AExp.beval [in Imp]
AExp.optimize_0plus [in Imp]
AExp.test_aeval1 [in Imp]
AExp.test_optimize_0plus [in Imp]
AExp.two_plus_two [in Imp]
AExp.two_plus_two' [in Imp]
andb [in Basics]
andb3 [in Basics]
antisymmetric [in Logic]
app [in Poly]
Assertion [in Hoare]
assn_sub [in Hoare]
assn_sub_example [in Hoare]
assn_sub_example' [in Hoare]
atrans_sound [in Equiv]
B
bassn [in Hoare]bequiv [in Equiv]
beq_id [in Imp]
beq_nat [in Basics]
beq_nat_sym [in Lists]
between [in Props]
beval [in Imp]
bind_option [in Imp]
ble_nat [in Basics]
ble_nat [in SfLib]
blt_nat [in Basics]
btrans_sound [in Equiv]
C
cequiv [in Equiv]ceval_example1 [in Imp]
ceval_example2 [in Imp]
ceval_step [in Imp]
ceval_step1 [in Imp]
ceval_step2 [in Imp]
classic [in Logic]
combine [in Poly]
constfun [in Poly]
context [in Subtyping]
countoddmembers' [in Poly]
ctrans_sound [in Equiv]
D
de_morgan_not_and_not [in Logic]doit3times [in Poly]
double [in Poly]
E
empty [in Subtyping]empty_state [in Imp]
equivalence [in Logic]
even [in Props]
evenb [in Basics]
even_n__even_SSn [in Props]
ev_plus4 [in Props]
ev_ten [in Props]
Examples.subtyping_example_0 [in Subtyping]
Examples.subtyping_example_1 [in Subtyping]
Examples.subtyping_example_2 [in Subtyping]
Examples.subtyping_example_3 [in Subtyping]
Examples.subtyping_example_4 [in Subtyping]
Examples.tm_rcd_kj [in Subtyping]
Examples.ty_rcd_j [in Subtyping]
Examples.ty_rcd_kj [in Subtyping]
Examples2.typing_example_0 [in Subtyping]
Examples2.typing_example_1 [in Subtyping]
Examples2.typing_example_2 [in Subtyping]
excluded_middle [in Logic]
exists_example_1 [in Logic]
exists_example_1' [in Logic]
exp [in Basics]
exp_body [in Imp]
extend [in Subtyping]
F
factorial [in Basics]Factorial.fact_body [in Hoare]
Factorial.fact_com [in Hoare]
Factorial.fact_loop [in Hoare]
Factorial.real_fact [in Hoare]
fact_body [in Imp]
fact_com [in Imp]
fact_invariant [in Equiv]
fact_loop [in Imp]
filter [in Poly]
find_parity [in Hoare]
find_parity_invariant [in Hoare]
find_parity_invariant' [in Hoare]
flat_map [in Poly]
fold [in Poly]
fold_aexp_ex1 [in Equiv]
fold_aexp_ex2 [in Equiv]
fold_bexp_ex1 [in Equiv]
fold_bexp_ex2 [in Equiv]
fold_com_ex1 [in Equiv]
fold_constants_aexp [in Equiv]
fold_constants_bexp [in Equiv]
fold_constants_com [in Equiv]
four_ev [in Props]
fst [in Poly]
H
has_type_nonexample [in Stlc]has_type_1 [in Stlc]
hd_opt [in Poly]
hoare_asgn_example1 [in Hoare]
hoare_asgn_example1' [in Hoare]
hoare_asgn_example2 [in Hoare]
hoare_asgn_example3 [in Hoare]
hoare_asgn_example4 [in Hoare]
hoare_triple [in Hoare]
I
iff [in Logic]if_exercise [in Hoare]
implies_to_or [in Logic]
index [in Poly]
L
length [in Poly]length' [in Poly]
loop [in Imp]
lt [in Logic]
l_123 [in Poly]
l_123' [in Poly]
l_123'' [in Poly]
M
map [in Poly]map_option [in Poly]
minustwo [in Basics]
mynil [in Poly]
MyProp_iff_ev [in Logic]
N
nandb [in Basics]NatList.add [in Lists]
NatList.alternate [in Lists]
NatList.app [in Lists]
NatList.bag [in Lists]
NatList.beq_natlist [in Lists]
NatList.count [in Lists]
NatList.countoddmembers [in Lists]
NatList.fst [in Lists]
NatList.fst' [in Lists]
NatList.hd [in Lists]
NatList.hd_opt [in Lists]
NatList.index [in Lists]
NatList.index' [in Lists]
NatList.index_bad [in Lists]
NatList.length [in Lists]
NatList.l_123 [in Lists]
NatList.l_123' [in Lists]
NatList.l_123'' [in Lists]
NatList.l_123''' [in Lists]
NatList.member [in Lists]
NatList.nonzeros [in Lists]
NatList.oddmembers [in Lists]
NatList.option_elim [in Lists]
NatList.remove_all [in Lists]
NatList.remove_one [in Lists]
NatList.repeat [in Lists]
NatList.rev [in Lists]
NatList.snd [in Lists]
NatList.snd' [in Lists]
NatList.snoc [in Lists]
NatList.subset [in Lists]
NatList.swap_pair [in Lists]
NatList.test_add1 [in Lists]
NatList.test_add2 [in Lists]
NatList.test_alternate1 [in Lists]
NatList.test_alternate2 [in Lists]
NatList.test_alternate3 [in Lists]
NatList.test_app1 [in Lists]
NatList.test_app2 [in Lists]
NatList.test_app3 [in Lists]
NatList.test_beq_natlist1 [in Lists]
NatList.test_beq_natlist2 [in Lists]
NatList.test_beq_natlist3 [in Lists]
NatList.test_countoddmembers1 [in Lists]
NatList.test_countoddmembers2 [in Lists]
NatList.test_countoddmembers3 [in Lists]
NatList.test_count1 [in Lists]
NatList.test_count2 [in Lists]
NatList.test_hd_opt1 [in Lists]
NatList.test_hd_opt2 [in Lists]
NatList.test_hd_opt3 [in Lists]
NatList.test_index1 [in Lists]
NatList.test_index2 [in Lists]
NatList.test_index3 [in Lists]
NatList.test_member1 [in Lists]
NatList.test_member2 [in Lists]
NatList.test_nonzeros [in Lists]
NatList.test_oddmembers [in Lists]
NatList.test_remove_all1 [in Lists]
NatList.test_remove_all2 [in Lists]
NatList.test_remove_all3 [in Lists]
NatList.test_remove_all4 [in Lists]
NatList.test_remove_one1 [in Lists]
NatList.test_remove_one2 [in Lists]
NatList.test_remove_one3 [in Lists]
NatList.test_remove_one4 [in Lists]
NatList.test_rev1 [in Lists]
NatList.test_rev2 [in Lists]
NatList.test_subset1 [in Lists]
NatList.test_subset2 [in Lists]
NatList.test_union1 [in Lists]
NatList.tl [in Lists]
NatList.union [in Lists]
nat_induction [in Props]
nat_induction_example [in Props]
negb [in Basics]
next_weekday [in Basics]
normalizing [in Smallstep]
normal_form [in Smallstep]
normal_form_of [in Smallstep]
not [in Logic]
no_whiles [in Imp]
O
oddb [in Basics]orb [in Basics]
order [in Logic]
override [in Imp]
override [in Poly]
P
partial_function [in SfLib]partial_function [in Logic]
peirce [in Logic]
pexp [in Imp]
Playground1.pred [in Basics]
Playground2.minus [in Basics]
Playground2.mult [in Basics]
Playground2.plus [in Basics]
plus2 [in Imp]
plus2_notation [in Imp]
plus3 [in Poly]
plus_fact [in Props]
preorder [in Logic]
preserved_by_S [in Props]
prod_curry [in Poly]
prod_uncurry [in Poly]
P_m0r [in Props]
P_m0r' [in Props]
R
real_fact [in Imp]real_fact [in Equiv]
reduce_to_zero [in Hoare]
reflexive [in Logic]
relation [in Logic]
repeat [in Poly]
RepeatExercise.hoare_triple [in Hoare]
rev [in Poly]
S
sillyex1 [in Poly]sillyex2 [in Poly]
sillyfun [in Poly]
sillyfun1 [in Poly]
SimpleArith2.test_step_1 [in Smallstep]
SimpleArith2.test_step_2 [in Smallstep]
snd [in Poly]
snoc [in Poly]
some_tm_is_stuck [in Stlc]
sqrt_com [in Hoare]
sqrt_inv [in Hoare]
sqrt_loop [in Hoare]
sqrt_spec [in Hoare]
ss_invariant [in Equiv]
state [in Imp]
stepmany [in Stlc]
STLCChecker.beq_ty [in MoreStlc]
STLCChecker.type_check [in MoreStlc]
STLCExtended.context [in MoreStlc]
STLCExtended.empty [in MoreStlc]
STLCExtended.extend [in MoreStlc]
STLCExtended.fact [in MoreStlc]
STLCExtended.fact_example [in MoreStlc]
STLCExtended.fact_typechecks [in MoreStlc]
STLCExtended.FirstTry.alist [in MoreStlc]
STLCExtended.map [in MoreStlc]
STLCExtended.map_example [in MoreStlc]
STLCExtended.map_typechecks [in MoreStlc]
STLCExtended.subst [in MoreStlc]
STLCExtended.tm_lookup [in MoreStlc]
STLCExtended.typing_example [in MoreStlc]
STLCExtended.typing_nonexample [in MoreStlc]
STLCExtended.typing_nonexample_2 [in MoreStlc]
STLCExtended.ty_lookup [in MoreStlc]
STLCExtended.weird_type [in MoreStlc]
STLC.closed [in Stlc]
STLC.context [in Stlc]
STLC.empty [in Stlc]
STLC.extend [in Stlc]
STLC.id_A [in Stlc]
STLC.id_AarrowA [in Stlc]
STLC.id_AarrowA_arrow_AarrowA [in Stlc]
STLC.k [in Stlc]
STLC.subst [in Stlc]
STLC.typing_example_1 [in Stlc]
STLC.typing_example_1' [in Stlc]
STLC.typing_example_2 [in Stlc]
STLC.typing_example_2_full [in Stlc]
STLC.typing_example_3 [in Stlc]
STLC.typing_nonexample_1 [in Stlc]
STLC.typing_nonexample_2 [in Stlc]
STLC.typing_nonexample_3 [in Stlc]
stuck [in Stlc]
subst [in Subtyping]
subst_aexp [in Equiv]
subst_aexp_ex [in Equiv]
subst_equiv_property [in Equiv]
subtract_slowly [in Imp]
subtract_slowly [in Hoare]
subtract_slowly_body [in Imp]
subtract_slowly_invariant [in Hoare]
subtract_3_from_5_slowly [in Imp]
succ_hastype_nat__hastype_nat [in Stlc]
symmetric [in Logic]
T
teen [in Props]Temp4.bool_step_prop1 [in Smallstep]
Temp4.bool_step_prop2 [in Smallstep]
Temp4.bool_step_prop3 [in Smallstep]
Temp4.Temp5.bool_step_prop4 [in Smallstep]
Temp4.Temp5.bool_step_prop4_holds [in Smallstep]
test_andb31 [in Basics]
test_andb32 [in Basics]
test_andb33 [in Basics]
test_andb34 [in Basics]
test_anon_fun [in Poly]
test_anon_fun' [in Poly]
test_ble_nat1 [in Basics]
test_ble_nat2 [in Basics]
test_ble_nat3 [in Basics]
test_blt_nat1 [in Basics]
test_blt_nat2 [in Basics]
test_blt_nat3 [in Basics]
test_countoddmembers'1 [in Poly]
test_countoddmembers'2 [in Poly]
test_countoddmembers'3 [in Poly]
test_doit3times1 [in Poly]
test_doit3times2 [in Poly]
test_doit3times4 [in Poly]
test_factorial1 [in Basics]
test_factorial2 [in Basics]
test_filter1 [in Poly]
test_filter2 [in Poly]
test_flat_map1 [in Poly]
test_hd_opt1 [in Poly]
test_hd_opt2 [in Poly]
test_index1 [in Poly]
test_index2 [in Poly]
test_index3 [in Poly]
test_length1 [in Poly]
test_length2 [in Poly]
test_map1 [in Poly]
test_map2 [in Poly]
test_map3 [in Poly]
test_mult1 [in Basics]
test_nandb1 [in Basics]
test_nandb2 [in Basics]
test_nandb3 [in Basics]
test_nandb4 [in Basics]
test_next_weekday [in Basics]
test_oddb1 [in Basics]
test_oddb2 [in Basics]
test_orb1 [in Basics]
test_orb2 [in Basics]
test_orb3 [in Basics]
test_orb4 [in Basics]
test_plus3 [in Poly]
test_plus3' [in Poly]
test_plus3'' [in Poly]
test_repeat1 [in Poly]
test_rev1 [in Poly]
test_rev2 [in Poly]
tm_lookup [in Subtyping]
transitive [in Logic]
trans_eq_example [in Poly]
trans_eq_example' [in Poly]
trans_eq_exercise [in Poly]
true_for_all_numbers [in Props]
true_for_n__true_for_Sn [in Props]
true_for_zero [in Props]
ty_lookup [in Subtyping]
V
value [in Stlc]X
X [in Imp]XtimesYinZ [in Imp]
Y
Y [in Imp]Z
Z [in Imp]Module Index
A
AExp [in Imp]C
Combined [in Smallstep]E
Examples [in Subtyping]Examples2 [in Subtyping]
Excerpt_From_Coq_Relations_Library [in Smallstep]
F
Factorial [in Hoare]FirstLe [in Logic]
FirstTry [in MoreStlc]
M
MumbleBaz [in Poly]MyEquality [in Logic]
N
NatList [in Lists]P
P [in Props]Playground1 [in Basics]
Playground2 [in Basics]
R
R [in Logic]RepeatExercise [in Hoare]
S
SimpleArith1 [in Smallstep]SimpleArith2 [in Smallstep]
STLC [in Stlc]
STLCArith [in Stlc]
STLCChecker [in MoreStlc]
STLCExtended [in MoreStlc]
T
Temp1 [in Smallstep]Temp2 [in Smallstep]
Temp3 [in Smallstep]
Temp4 [in Smallstep]
Temp5 [in Smallstep]
Library Index
B
BasicsE
EquivH
HoareI
ImpL
ListsLogic
M
MoreStlcP
PolyPreface
Props
S
SfLibSmallstep
Stlc
Subtyping
| 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 | _ | (1294 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 | _ | (391 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 | _ | (348 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 | _ | (101 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 | _ | (42 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 | _ | (371 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 | _ | (27 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 | _ | (14 entries) |
This page has been generated by coqdoc