From 04b918431264facd78c2a54ca2fba0c3889fdc00 Mon Sep 17 00:00:00 2001 From: Philip Wadler Date: Tue, 4 Jul 2017 12:59:55 +0100 Subject: [PATCH] updated --- out/Basics.md | 30 ++++++++++++++++++++---------- 1 file changed, 20 insertions(+), 10 deletions(-) diff --git a/out/Basics.md b/out/Basics.md index bf0432d4..688d29e3 100644 --- a/out/Basics.md +++ b/out/Basics.md @@ -4,7 +4,8 @@ layout : page permalink : /Basics --- -
{% raw %}
+
+
 open)
-{% endraw %}

+
+
The functional programming style brings programming closer to simple, everyday mathematics: If a procedure or method has no side @@ -87,7 +89,8 @@ very simple example. The following declaration tells Agda that we are defining a new set of data values -- a *type*. -
{% raw %}
+
+
 dataDay
-{% endraw %}

+
+
The type is called `day`, and its members are `monday`, `tuesday`, etc. The second and following lines of the definition @@ -207,7 +211,8 @@ can be read "`monday` is a `day`, `tuesday` is a `day`, etc." Having defined `day`, we can write functions that operate on days. -
{% raw %}
+
+
 nextWeekdaymonday
-{% endraw %}

+
+
One thing to note is that the argument and return types of this function are explicitly declared. Like most functional @@ -369,7 +375,8 @@ above example to Agda, and observe the result. Second, we can record what we *expect* the result to be in the form of an Agda type: -
{% raw %}
+
+
 test_nextWeekdaytuesday
-{% endraw %}

+
+
This declaration does two things: it makes an assertion (that the second weekday after `saturday` is `tuesday`), and it gives the assertion a name @@ -410,7 +418,8 @@ that can be used to refer to it later. Having made the assertion, we must also verify it. We do this by giving a term of the above type: -
{% raw %}
+
+
 test_nextWeekdayrefl
-{% endraw %}

+
+
There is no essential difference between the definition for `test_nextWeekday` here and the definition for `nextWeekday` above,