equal
deleted
inserted
replaced
379 Write a function which takes two terms representing natural numbers |
379 Write a function which takes two terms representing natural numbers |
380 in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produce the |
380 in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produce the |
381 number representing their sum. |
381 number representing their sum. |
382 \end{exercise} |
382 \end{exercise} |
383 |
383 |
|
384 |
|
385 (FIXME: operation from page 19 of the implementation manual) |
384 *} |
386 *} |
385 |
387 |
386 section {* Type-Checking *} |
388 section {* Type-Checking *} |
387 |
389 |
388 text {* |
390 text {* |
426 |
428 |
427 \begin{exercise} |
429 \begin{exercise} |
428 Check that the function defined in Exercise~\ref{fun:revsum} returns a |
430 Check that the function defined in Exercise~\ref{fun:revsum} returns a |
429 result that type-checks. |
431 result that type-checks. |
430 \end{exercise} |
432 \end{exercise} |
|
433 |
|
434 (FIXME: @{text "ctyp_of"}) |
431 |
435 |
432 *} |
436 *} |
433 |
437 |
434 section {* Theorems *} |
438 section {* Theorems *} |
435 |
439 |
501 section {* Operations on Constants (Names) *} |
505 section {* Operations on Constants (Names) *} |
502 |
506 |
503 text {* |
507 text {* |
504 |
508 |
505 @{ML_response [display] "Sign.base_name \"List.list.Nil\"" "\"Nil\""} |
509 @{ML_response [display] "Sign.base_name \"List.list.Nil\"" "\"Nil\""} |
|
510 |
|
511 authentic syntax |
506 |
512 |
507 *} |
513 *} |
508 |
514 |
509 section {* Combinators\label{sec:combinators} *} |
515 section {* Combinators\label{sec:combinators} *} |
510 |
516 |
529 |
535 |
530 ML{*fun K x = fn _ => x*} |
536 ML{*fun K x = fn _ => x*} |
531 |
537 |
532 text {* |
538 text {* |
533 @{ML K} ``wraps'' a function around the argument @{text "x"}. However, this |
539 @{ML K} ``wraps'' a function around the argument @{text "x"}. However, this |
534 function ignores its argument. So @{ML K} defines a constant function |
540 function ignores its argument. As a result @{ML K} defines a constant function |
535 returning @{text x}. |
541 returning @{text x}. |
536 |
542 |
537 The next combinator is reverse application, @{ML "|>"}, defined as |
543 The next combinator is reverse application, @{ML "|>"}, defined as |
538 *} |
544 *} |
539 |
545 |
583 |
589 |
584 |
590 |
585 (FIXME: give a real world example involving theories) |
591 (FIXME: give a real world example involving theories) |
586 |
592 |
587 Similarly, the combinator @{ML "#>"} is the reverse function |
593 Similarly, the combinator @{ML "#>"} is the reverse function |
588 composition. It can be used to define functions as follows |
594 composition. It can be used to define the following function |
589 *} |
595 *} |
590 |
596 |
591 ML{*val inc_by_six = |
597 ML{*val inc_by_six = |
592 (fn x => x + 1) |
598 (fn x => x + 1) |
593 #> (fn x => x + 2) |
599 #> (fn x => x + 2) |
658 ML{*fun double x = |
664 ML{*fun double x = |
659 x |> (fn x => (x, x)) |
665 x |> (fn x => (x, x)) |
660 |-> (fn x => fn y => x + y)*} |
666 |-> (fn x => fn y => x + y)*} |
661 |
667 |
662 text {* |
668 text {* |
663 Recall that @{ML "|>"} is the reverse function applications. The related |
669 Recall that @{ML "|>"} is the reverse function applications. Recall also that the related |
664 reverse function composition is @{ML "#>"}. In fact all combinators @{ML "|->"}, |
670 reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"}, |
665 @{ML "|>>"} and @{ML "||>"} described above have related combinators for function |
671 @{ML "|>>"} and @{ML "||>"} described above have related combinators for function |
666 composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "|->"}, |
672 composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "#->"}, |
667 the function @{text double} can also be written as |
673 for example, the function @{text double} can also be written as |
668 *} |
674 *} |
669 |
675 |
670 ML{*val double = |
676 ML{*val double = |
671 (fn x => (x, x)) |
677 (fn x => (x, x)) |
672 #-> (fn x => fn y => x + y)*} |
678 #-> (fn x => fn y => x + y)*} |