isabelle-cookbook: comparison ProgTutorial/FirstSteps.thy

equal deleted inserted replaced

-:1fb8d62c88a0
+:ce0f60d0351e
 ((fn x => x + 4) o fst o (fn x => (x, x)) o (fn x => x + 1)) x*}
 text {* and typographically more economical than *}
 ML{*fun inc_by_five x =
 let val y1 = x + 1
 val y2 = (y1, y1)
 val y3 = fst y2
 val y4 = y3 + 4
 in y4 end*}
 text {*
 Another reason why the let-bindings in the code above are better to be
 avoided: it is more than easy to get the intermediate values wrong, not to
 mention the nightmares the maintenance of this code causes!
 f |> fastype_of
 |> binder_types
 |> map (pair "z")
 |> Variable.variant_frees ctxt [f]
 |> map Free
-|> (curry list_comb) f *}
+|> curry list_comb f *}
 text {*
 This code extracts the argument types of a given function @{text "f"} and then generates
 for each argument type a distinct variable; finally it applies the generated
 variables to the function. For example:
 end"
 "99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006,
 100007, 100008, 100009, 100010, 100011, 100012, 100013, 100014, 100015,
 100016, 100017, 100018, 100019, 100020"}
-where @{ML upto} generates a list of integers. You can print this
+where @{ML upto} generates a list of integers. You can print out this
-list out as an ``set'', that means enclosed inside @{text [quotes] "{"} and
+list as an ``set'', that means enclosed inside @{text [quotes] "{"} and
 @{text [quotes] "}"}, and separated by commas using the function
 @{ML [index] enum in Pretty}. For example
 *}
 text {*
 "{99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006,
 100007, 100008, 100009, 100010, 100011, 100012, 100013, 100014, 100015,
 100016, 100017, 100018, 100019, 100020}"}
 As can be seen, this function prints out the ``set'' so that starting
-from the second each new line as an indentation of 2.
+from the second, each new line as an indentation of 2.
-If you print something out which goes beyond the capabilities of the
+If you print out something that goes beyond the capabilities of the
-standard function, you can do realatively easily the formating
+standard functions, you can do realatively easily the formating
 yourself. Assume you want to print out a list of items where like in ``English''
 the last two items are separated by @{text [quotes] "and"}. For this you can
 write the function
 *}
 (Pretty.commas front) @
 [Pretty.brk 1, Pretty.str "and", Pretty.brk 1, last]
 end *}
 text {*
-where in Line 7 we print the beginning of the list and in Line
+where Line 7 prints the beginning of the list and Line
 8 the last item. We have to use @{ML "Pretty.brk 1"} in order
 to insert a space (of length 1) before the
 @{text [quotes] "and"}. This space is also a pleace where a linebreak
 can occur. We do the same ater the @{text [quotes] "and"}. This gives you
 for example
 (pstr "The term " @ [ptrm] @ pstr " has type "
 @ [pty, Pretty.str "."])))
 end*}
 text {*
-In Line 3 we define a function that inserts according to spaces
+In Line 3 we define a function that inserts possible linebreaks in places
-possible linebreaks into an (English). In Lines 4 and 5 we pretty-print
+where a space is. In Lines 4 and 5 we pretty-print the term and its type
-the term and its type using the functions @{ML [index] pretty_term in Syntax} and
+using the functions @{ML [index] pretty_term in Syntax} and @{ML [index]
-@{ML [index] pretty_typ in Syntax}. We also use the function @{ML [index] quote in Pretty}
+pretty_typ in Syntax}. We also use the function @{ML [index] quote in
-in order to enclose the term and type inside quotation marks. In Line
+Pretty} in order to enclose the term and type inside quotation marks. In
-9 we add a period right after the type without the possibility of a
+Line 9 we add a period right after the type without the possibility of a
 linebreak, because we do not want that a linebreak occurs there.
 Now you can write
 @{ML_response_fake [display,gray]
 "tell_type @{context} @{term \"min (Suc 0)\"}"
 @{ML_response_fake [display,gray]
 "tell_type @{context} @{term \"op = (op = (op = (op = (op = op =))))\"}"
 "The term \"op = (op = (op = (op = (op = op =))))\" has type
 \"((((('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool\"."}
+FIXME: TBD below
 *}
 ML {* pprint (Pretty.big_list "header"  (map (Pretty.str o string_of_int) (4 upto 10))) *}
 text {*

changeset 257	ce0f60d0351e
parent 256	1fb8d62c88a0
child 258	03145998190b