ProgTutorial/Essential.thy
changeset 446 4c32349b9875
parent 441 520127b708e6
child 448 957f69b9b7df
--- a/ProgTutorial/Essential.thy	Fri Aug 13 18:05:30 2010 +0800
+++ b/ProgTutorial/Essential.thy	Fri Aug 13 18:42:58 2010 +0800
@@ -632,6 +632,14 @@
   number representing their sum.
   \end{exercise}
 
+  \begin{exercise}\label{fun:makelist}
+  Write a function that takes an integer @{text i} and
+  produces an Isabelle integer list from @{text 1} upto @{text i}, 
+  and then builds the reverse of this list using @{const rev}. 
+  The relevant helper functions are @{ML upto}, 
+  @{ML HOLogic.mk_number} and @{ML HOLogic.mk_list}.
+  \end{exercise}
+
   \begin{exercise}\label{ex:debruijn}
   Implement the function, which we below name deBruijn, that depends on a natural
   number n$>$0 and constructs terms of the form: