updated

out/Basics.md

@@ -4,7 +4,8 @@ layout    : page
 permalink : /Basics
 ---
 
-<pre class="Agda">{% raw %}
+<pre class="Agda">
+
 <a name="113" class="Keyword"
       >open</a
       ><a name="117"
@@ -34,7 +35,8 @@ permalink : /Basics
       ><a name="179" class="Symbol"
       >)</a
       >
-{% endraw %}</pre>
+
+</pre>
 
 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*.
 
-<pre class="Agda">{% raw %}
+<pre class="Agda">
+
 <a name="2469" class="Keyword"
       >data</a
       ><a name="2473"
@@ -198,7 +201,8 @@ a new set of data values -- a *type*.
       ><a name="2612" href="Basics.html#2474" class="Datatype"
       >Day</a
       >
-{% endraw %}</pre>
+
+</pre>
 
 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.
 
-<pre class="Agda">{% raw %}
+<pre class="Agda">
+
 <a name="2894" href="Basics.html#2894" class="Function"
       >nextWeekday</a
       ><a name="2905"
@@ -346,7 +351,8 @@ days.
       ><a name="3135" href="Basics.html#2492" class="InductiveConstructor"
       >monday</a
       >
-{% endraw %}</pre>
+
+</pre>
 
 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:
 
-<pre class="Agda">{% raw %}
+<pre class="Agda">
+
 <a name="4097" href="Basics.html#4097" class="Function Operator"
       >test_nextWeekday</a
       ><a name="4113"
@@ -401,7 +408,8 @@ form of an Agda type:
       ><a name="4153" href="Basics.html#2510" class="InductiveConstructor"
       >tuesday</a
       >
-{% endraw %}</pre>
+
+</pre>
 
 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:
 
-<pre class="Agda">{% raw %}
+<pre class="Agda">
+
 <a name="4472" href="Basics.html#4097" class="Function Operator"
       >test_nextWeekday</a
       ><a name="4488"
@@ -422,7 +431,8 @@ a term of the above type:
       ><a name="4491" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
       >refl</a
       >
-{% endraw %}</pre>
+
+</pre>
 
 There is no essential difference between the definition for
 `test_nextWeekday` here and the definition for `nextWeekday` above,