doc-src/TutorialI/todo.tobias
changeset 10971 6852682eaf16
parent 10855 140a1ed65665
child 10983 59961d32b1ae
equal deleted inserted replaced
10970:7917e66505a4 10971:6852682eaf16
    87 
    87 
    88 Possible exercises
    88 Possible exercises
    89 ==================
    89 ==================
    90 
    90 
    91 Exercises
    91 Exercises
    92 %\begin{exercise}
    92 
    93 %Extend expressions by conditional expressions.
    93 For extensionality (in Sets chapter): prove
    94 braucht wfrec!
    94 valif o norm = valif
    95 %\end{exercise}
    95 in If-expression case study (Ifexpr)
    96 
    96 
    97 Nested inductive datatypes: another example/exercise:
    97 Nested inductive datatypes: another example/exercise:
    98  size(t) <= size(subst s t)?
    98  size(t) <= size(subst s t)?
    99 
    99 
   100 insertion sort: primrec, later recdef
   100 insertion sort: primrec, later recdef