equal
deleted
inserted
replaced
32 |
32 |
33 text {* \solution{fun:makesum} *} |
33 text {* \solution{fun:makesum} *} |
34 |
34 |
35 ML{*fun make_sum t1 t2 = |
35 ML{*fun make_sum t1 t2 = |
36 HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *} |
36 HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *} |
|
37 |
|
38 |
|
39 text {* \solution{fun:makelist} *} |
|
40 |
|
41 ML{*fun mk_rev_upto i = |
|
42 1 upto i |
|
43 |> map (HOLogic.mk_number @{typ int}) |
|
44 |> HOLogic.mk_list @{typ int} |
|
45 |> curry (op $) @{term "rev :: int list \<Rightarrow> int list"}*} |
37 |
46 |
38 text {* \solution{ex:debruijn} *} |
47 text {* \solution{ex:debruijn} *} |
39 |
48 |
40 ML{*fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) |
49 ML{*fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) |
41 |
50 |