Here is a list of bugs that occured in assignments and their solutions so far.
Note that all of them have been fixed in the versions now online.

If you find additional mistakes, please let us know.


Assignments:

* 8.0: In the syntax definition for terms and values it should read lambda X.t
  instead of lambda X.T.

* 8.1: case t t1 t2 needs a where clause:
    where Gamma |- ti : Ti->T

* 8.9: The universal quantifier should be a lambda:
    id = \X.\x:X.x

* 9.0: In the grammar for types T, it should be \X:k.T instead of \X:k.t.

* 9.0: In the grammar for type reduction contexts R, it should be forall X:k.R
  instead of forall X:k.T.

* 9.4: In the application of imp, the type lambda for X should have a kind
  annotation, X:k.

* 10.7: Identical copy of 10.4, please ignore.

* 10.11.c): The kind of Sig should be *->*, and it should say "...such that
  Sig represents..." instead of "...such that Sig T represents...".

* 11.0: In the definition of Church-Rosser, replace y<->*y with x<->*y.

* 11.0: The definition of "-> terminates on x" was missing:
  -> termniates on x <=> not exists A subset X: x in A and forall x in A: ...

* 11.0: In the definition of "-> terminates" we must demand A non-empty.
  Alternatively, we can define
    -> terminates  <=>  forall t: -> terminates on t

* 11.5: Condition (2) should say "For every P, ..." instead of having P
  chosen a priori. Furthermore, we require Dom(>) subset X.

* 12.3: The type for datatype ty should be
    datatype ty = TV of tyvar | Arrow of ty * ty

* 13.2.b): Replace the question with:
    Is there any principal solution with TV(Con sigma) <= {X,Y,Z}
    that is not idempotent?


Solutions:

* 1.1.e): There must be a c0 instead of c1, i.e.
    pre = fst ( n g (pair c0 c0) )

* 1.1.h): There is an "n" missing, it should be
    foo = \n.n (\x.xx) (\x.xx)

* 1.2.d): The application of rev should be to the initial l, not to the result:
    tl = \l.snd(rev l g (pair nil nil))

* 2.2.b(iv): The solution should read
    \(\2301)(\02)21

* 3.1.e): The context should better be (\f.\x.*) Omega' I.

* 5.6: The branches for the if were the wrong way round.

* 5.7.b): The first argument to "case", a, was missing.

* 5.7.c): The first argument to "case", b, was missing.

* 5.7.e): A closing parenthesis was missing.

* 5.10.a): The application was the wrong way round.

* 6.1.b): It should be v::R instead of v::t

* 6.1.d): In the premises of the lcase rules it should just say t instead of t1.

* 6.2.f): Sum type values should be formed as (i,t) instead of (i,v).

* 6.4.e): Change "v v" to "v v'" in the premise of the second try rule.

* 6.4.f): Change the substitution to "[x:=v2]" in the premise of the first rule.

* 6.4.g): Replace Gamma with the empty set in accordance with our definitions.

* 6.4.h): The recursive procedure must be applied to (); change the type
  annotation of x to 1.

* 7.3.a): "R.i" is missing from the reduction context.

* 7.3.i): The second \m:Nat.t should bind n.

* 8.2): The second premise in the second rule should be t_2||v_2; the conclusion
  in the third rule should be t_1 T||v.

* 8.10.f): The constructor V in the implementation of substTy procedure must
  be X.

* 9.5.b): In the rule for variables, it should be Gamma(x) instead of Gamma(s).

* 9.5.c): In the rule for variables, the resulting type has to be
  up(n+1) Gamma.(n+1) instead of Gamma.n.

* 9.7.b): The definition of occurs lacks a constructor call. It should be
    fun occurs n e = subst 0 (fn n' => V(if n' = n then n'+1 else n')) e <> e

* 9.7.b): In the definiton of norm, we need to lower free variables when we do
  eta reduction. That is, replace the "else e1" in the first case with
  "else up ~1 e1".

* 9.8.a): Name head and tail function in accordance with the exercise. The
  take' function should only deliver "rev l" instead of a pair.

* 10.1.b): In the last line it has to be m^2 instead of m^3.

* 10.10: In case 2, item 3 it should say R[t1t2] = t1t2.

* 10.12.o): The final application should be f A B C y x.

* 11.1.a): In (ii), remove the quantor for x.

* 11.1.b): In the case T1->T2, proving A2, remove the bogus reference to (1) at
  the induction step.

* 11.1.c): The proof for the lambda case was showing the wrong thing. Later,
  we forgot to prove (S theta' t') : T', as a prerequisite for Lemma B.

* 13.5.a): In the premise of the first rule, the type should be T1, not t1.

* 14.9.b): Added alternative rule. Fixed premise screwed up with the first
  correction.

* 14.9.g): Since we have Top, there certainly is a type like that, namely
    Sigma {l1:Top,...,ln:Top}