Exam
Requirements met for final assessment:
- wild boar, cuckoo, bufflehead, locust (checked on Dec 16th)
- vulture, shearwater, adder (checked on Jan 19th)
Exercises
- Basics.v
- Definition, Fixpoint, simpl, reflexivity: nandb, test_nandb*,andb3, test_andb3*, factorial, test_factorial*
- intros, rewrite: plus_id_exercise, mult_S_1
- destruct: andb_true_elim2, zero_nbeq_plus_1, andb_eq_orb
- Induction.v
- induction: mult_0_r, plus_n_Sm, plus_comm, plus_assoc, double_plus, evenb_S
- Lists.v
- snd_fst_is_swap, fst_swap_is_snd
- app_nil_r, rev_app_distr, rev_involutive
- Tactics.v (also requires Poly.v)
- apply:silly_ex, rev_exercise1
- injection, discriminate: injection_ex_3, discriminate_ex_3
- IndProp.v (also requires Logic.v)
- inversion: SSSSev__even, even5_nonsense
- Theory Exercise 1 (tex)
- Deadline: Oct. 9th
- Smallstep.v (also requires Maps.v and Imp.v)
- value_not_same_as_normal_form (three versions), multistep_congr_2, eval__multistep, step__eval, multistep__eval
- Types.v
- value_is_nf, progress, preservation
- Stlc.v
- step_example5, typing_example_2_full, typing_example_3, typing_nonexample_3
- StlcProp.v
- progress', typable_empty__closed, soundness, unique_types
- StlcArith
- progress, preservation
- MoreStlc.v
- complete: subst, step, has_type, progress, appears_free_in, context_invariance, free_in_context, substitution_preserves_typing, preservation
- Theory Exercise 2 (tex)
- Deadline: Nov. 20th
- DepT.v
- vtail', vtail, vmap, unzip, tabulate, get, ev_eq, IsT1, IsTP, rewriteNat, IsTL, IsTAddOne, IsTLR, insert'_induction, insert, sort
- RecordSub.v
- sub_inversion_arrow, canonical_forms_of_arrow_types
Sellele ülesandele ei saa enam lahendusi esitada.
2. Induction.v
Sellele ülesandele ei saa enam lahendusi esitada.
3. Lists.v
Sellele ülesandele ei saa enam lahendusi esitada.
4. Tactics.v
Sellele ülesandele ei saa enam lahendusi esitada.
5. IndProp.v
Sellele ülesandele ei saa enam lahendusi esitada.
6. Exercise1
Sellele ülesandele ei saa enam lahendusi esitada.
7. Smallstep.v
Sellele ülesandele ei saa enam lahendusi esitada.
8. Types.v
Sellele ülesandele ei saa enam lahendusi esitada.
9. Stlc.v
Sellele ülesandele ei saa enam lahendusi esitada.
10. StlcProp.v
Sellele ülesandele ei saa enam lahendusi esitada.
11. StlcArith.v
Sellele ülesandele ei saa enam lahendusi esitada.
12. MoreStlc.v
Sellele ülesandele ei saa enam lahendusi esitada.
13. Exercise2
Sellele ülesandele ei saa enam lahendusi esitada.
14. DepT.v
Sellele ülesandele ei saa enam lahendusi esitada.
15. RecordSub.v
Sellele ülesandele ei saa enam lahendusi esitada.
16. ExamDecember
Sellele ülesandele ei saa enam lahendusi esitada.
17. ExamJanuary
Sellele ülesandele ei saa enam lahendusi esitada.