doc-src/TutorialI/todo.tobias
changeset 10971 6852682eaf16
parent 10855 140a1ed65665
child 10983 59961d32b1ae
     1.1 --- a/doc-src/TutorialI/todo.tobias	Wed Jan 24 11:59:15 2001 +0100
     1.2 +++ b/doc-src/TutorialI/todo.tobias	Wed Jan 24 12:29:10 2001 +0100
     1.3 @@ -89,10 +89,10 @@
     1.4  ==================
     1.5  
     1.6  Exercises
     1.7 -%\begin{exercise}
     1.8 -%Extend expressions by conditional expressions.
     1.9 -braucht wfrec!
    1.10 -%\end{exercise}
    1.11 +
    1.12 +For extensionality (in Sets chapter): prove
    1.13 +valif o norm = valif
    1.14 +in If-expression case study (Ifexpr)
    1.15  
    1.16  Nested inductive datatypes: another example/exercise:
    1.17   size(t) <= size(subst s t)?