equal
deleted
inserted
replaced
628 |
628 |
629 \begin{exercise}\label{fun:makesum} |
629 \begin{exercise}\label{fun:makesum} |
630 Write a function that takes two terms representing natural numbers |
630 Write a function that takes two terms representing natural numbers |
631 in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the |
631 in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the |
632 number representing their sum. |
632 number representing their sum. |
|
633 \end{exercise} |
|
634 |
|
635 \begin{exercise}\label{fun:makelist} |
|
636 Write a function that takes an integer @{text i} and |
|
637 produces an Isabelle integer list from @{text 1} upto @{text i}, |
|
638 and then builds the reverse of this list using @{const rev}. |
|
639 The relevant helper functions are @{ML upto}, |
|
640 @{ML HOLogic.mk_number} and @{ML HOLogic.mk_list}. |
633 \end{exercise} |
641 \end{exercise} |
634 |
642 |
635 \begin{exercise}\label{ex:debruijn} |
643 \begin{exercise}\label{ex:debruijn} |
636 Implement the function, which we below name deBruijn, that depends on a natural |
644 Implement the function, which we below name deBruijn, that depends on a natural |
637 number n$>$0 and constructs terms of the form: |
645 number n$>$0 and constructs terms of the form: |