648 Abs (\"x\", \<dots>, |
648 Abs (\"x\", \<dots>, |
649 Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ |
649 Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ |
650 (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"} |
650 (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"} |
651 |
651 |
652 There are a number of handy functions that are frequently used for |
652 There are a number of handy functions that are frequently used for |
653 constructing terms. One is the function @{ML list_comb} which a term |
653 constructing terms. One is the function @{ML list_comb} which takes a term |
654 and a list of terms as argument, and produces as output the term |
654 and a list of terms as arguments, and produces as output the term |
655 list applied to the term. For example |
655 list applied to the term. For example |
656 |
656 |
657 @{ML_response_fake [display,gray] |
657 @{ML_response_fake [display,gray] |
658 "list_comb (@{term \"P::nat\"}, [@{term \"True\"}, @{term \"False\"}])" |
658 "list_comb (@{term \"P::nat\"}, [@{term \"True\"}, @{term \"False\"}])" |
659 "Free (\"P\", \"nat\") $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"} |
659 "Free (\"P\", \"nat\") $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"} |
686 associates to the left. Try your function on some examples. |
686 associates to the left. Try your function on some examples. |
687 \end{exercise} |
687 \end{exercise} |
688 |
688 |
689 \begin{exercise}\label{fun:makesum} |
689 \begin{exercise}\label{fun:makesum} |
690 Write a function which takes two terms representing natural numbers |
690 Write a function which takes two terms representing natural numbers |
691 in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produce the |
691 in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the |
692 number representing their sum. |
692 number representing their sum. |
693 \end{exercise} |
693 \end{exercise} |
694 |
694 |
695 There are a few subtle issues with constants. They usually crop up when |
695 There are a few subtle issues with constants. They usually crop up when |
696 pattern matching terms or types, or when constructing them. While it is perfectly ok |
696 pattern matching terms or types, or when constructing them. While it is perfectly ok |