diff --git a/out/Basics.md b/out/Basics.md index 688d29e3..bf0432d4 100644 --- a/out/Basics.md +++ b/out/Basics.md @@ -4,8 +4,7 @@ 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 @@ -89,8 +87,7 @@ 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 @@ -211,8 +207,7 @@ 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 @@ -375,8 +369,7 @@ 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 @@ -418,8 +410,7 @@ 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, diff --git a/out/Maps.md b/out/Maps.md index 76d793b3..4d894678 100644 --- a/out/Maps.md +++ b/out/Maps.md @@ -32,8 +32,7 @@ much difference, though, because we've been careful to name our own definitions and theorems the same as their counterparts in the standard library, wherever they overlap. -
-
+
{% raw %}
 open; ⊥-elim))
-
-

+{% endraw %}
Documentation for the standard library can be found at . @@ -256,8 +254,7 @@ maps. For this purpose, we again use the type `Id` from the [Lists](sf/Lists.html) chapter. To make this chapter self contained, we repeat its definition here. -
-
+
{% raw %}
 dataId
-
-

+{% endraw %}
We recall a standard fact of logic. -
-
+
{% raw %}
 contrapositive)
-
-

+{% endraw %}
Using the above, we can decide equality of two identifiers by deciding equality on the underlying strings. -
-
+
{% raw %}
 _≟_refl
-
-

+{% endraw %}
We define some identifiers for future use. -
-
+
{% raw %}
 x"z"
-
-

+{% endraw %}
## Total Maps @@ -837,8 +827,7 @@ We build partial maps in two steps. First, we define a type of _total maps_ that return a default value when we look up a key that is not present in the map. -
-
+
{% raw %}
 TotalMapA
-
-

+{% endraw %}
Intuitively, a total map over anfi element type `A` _is_ just a function that can be used to look up ids, yielding `A`s. -
-
+
{% raw %}
 modulewhere
-
-

+{% endraw %}
The function `always` yields a total map given a default element; this map always returns the default element when applied to any id. -
-
+
{% raw %}
   alwaysv
-
-

+{% endraw %}
More interesting is the update function, which (as before) takes a map `ρ`, a key `x`, and a value `v` and returns a new map that takes `x` to `v` and takes every other key to whatever `ρ` does. -
-
+
{% raw %}
   infixly
-
-

+{% endraw %}
This definition is a nice example of higher-order programming. The update function takes a _function_ `ρ` and yields a new @@ -1162,8 +1144,7 @@ function that behaves like the desired map. For example, we can build a map taking ids to naturals, where `x` maps to 42, `y` maps to 69, and every other key maps to 0, as follows: -
-
+
{% raw %}
   ρ₀69
-
-

+{% endraw %}
This completes the definition of total maps. Note that we don't need to define a `find` operation because it is just function application! -
-
+
{% raw %}
   test₁refl
-
-

+{% endraw %}
To use maps in later chapters, we'll need several fundamental facts about how they behave. Even if you don't work the following @@ -1362,8 +1340,7 @@ the lemmas! #### Exercise: 1 star, optional (apply-always) The `always` map returns its default element for all keys: -
-
+
{% raw %}
   postulatev
-
-

+{% endraw %}
#### Exercise: 2 stars, optional (update-eq) @@ -1555,8 +1529,7 @@ Next, if we update a map `ρ` at a key `x` with a new value `v` and then look up `x` in the map resulting from the update, we get back `v`: -
-
+
{% raw %}
   postulatev
-
-

+{% endraw %}
#### Exercise: 2 stars, optional (update-neq) @@ -1896,8 +1866,7 @@ On the other hand, if we update a map `m` at a key `x` and then look up a _different_ key `y` in the resulting map, we get the same result that `m` would have given: -
-
+
{% raw %}
   update-neq= ⊥-elim refl
-
-

+{% endraw %}
For the following lemmas, since maps are represented by functions, to show two maps equal we will need to postulate extensionality. -
-
+
{% raw %}
   postulateρ′
-
-

+{% endraw %}
#### Exercise: 2 stars, optional (update-shadow) If we update a map `ρ` at a key `x` with a value `v` and then @@ -2277,8 +2243,7 @@ resulting map behaves the same (gives the same result when applied to any key) as the simpler map obtained by performing just the second update on `ρ`: -
-
+
{% raw %}
   postulate)
-
-

+{% endraw %}
#### Exercise: 2 stars (update-same) @@ -2829,8 +2791,7 @@ Prove the following theorem, which states that if we update a map `ρ` to assign key `x` the same value as it already has in `ρ`, then the result is equal to `ρ`: -
-
+
{% raw %}
   postulateρ
-
-

+{% endraw %}
#### Exercise: 3 stars, recommended (update-permute) @@ -3211,8 +3169,7 @@ Prove one final property of the `update` function: If we update a map `m` at two distinct keys, it doesn't matter in which order we do the updates. -
-
+
{% raw %}
   postulate)
-
-

+{% endraw %}
## Partial maps @@ -4710,8 +4662,7 @@ Finally, we define _partial maps_ on top of total maps. A partial map with elements of type `A` is simply a total map with elements of type `Maybe A` and default element `nothing`. -
-
+
{% raw %}
 PartialMap)
+{% endraw %}

 
-
- -
-
+
{% raw %}
 modulewhere
+{% endraw %}

 
-
- -
-
+
{% raw %}
   ∅nothing
+{% endraw %}

 
-
- -
-
+
{% raw %}
   infixl)
-
-

+{% endraw %}
We now lift all of the basic lemmas about total maps to partial maps. -
-
+
{% raw %}
   apply-∅x
+{% endraw %}

 
-
- -
-
+
{% raw %}
   update-eq)
+{% endraw %}

 
-
- -
-
+
{% raw %}
   update-neqx≢y
+{% endraw %}

 
-
- -
-
+
{% raw %}
   update-shadow)
+{% endraw %}

 
-
- -
-
+
{% raw %}
   update-samex
+{% endraw %}

 
-
- -
-
+
{% raw %}
   update-permutex≢y
-
-

+{% endraw %}