ProgTutorial/Solutions.thy
changeset 446 4c32349b9875
parent 441 520127b708e6
child 447 d21cea8e0bcf
--- a/ProgTutorial/Solutions.thy	Fri Aug 13 18:05:30 2010 +0800
+++ b/ProgTutorial/Solutions.thy	Fri Aug 13 18:42:58 2010 +0800
@@ -35,6 +35,15 @@
 ML{*fun make_sum t1 t2 =
       HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *}
 
+
+text {* \solution{fun:makelist} *}
+
+ML{*fun mk_rev_upto i = 
+  1 upto i
+  |> map (HOLogic.mk_number @{typ int})
+  |> HOLogic.mk_list @{typ int}
+  |> curry (op $) @{term "rev :: int list \<Rightarrow> int list"}*}
+
 text {* \solution{ex:debruijn} *}
 
 ML{*fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n)