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,