From eceafb86ebf5d707b470956da24611020a4bf6ba Mon Sep 17 00:00:00 2001 From: wadler Date: Thu, 6 Jul 2017 23:13:06 +0100 Subject: [PATCH] pushing html --- out/Maps.md | 7827 +++++++++++++++++++++++------------------------ out/Stlc.md | 5403 +++++++++++++++----------------- out/StlcProp.md | 6396 +++++++++++++++++++++----------------- 3 files changed, 9928 insertions(+), 9698 deletions(-) diff --git a/out/Maps.md b/out/Maps.md index 9115afbd..eb38d314 100644 --- a/out/Maps.md +++ b/out/Maps.md @@ -134,112 +134,87 @@ standard library, wherever they overlap. >import Data.String Relation.Nullary using (String) -open import Relation.Nullary using (¬_; Dec; yes; no) open import Relation.Binary.PropositionalEquality using (_≡_; refl; _≢_; trans; sym) {% endraw %} @@ -255,44 +230,44 @@ maps. For this purpose, we again use the type `Id` from the we repeat its definition here. 
{% raw %}
-data Id : Set where
   id : Stringℕ → Id
 {% endraw %}
@@ -300,152 +275,152 @@ we repeat its definition here. We recall a standard fact of logic. 
{% raw %}
-contrapositive : ∀ {ℓ₁ ℓ₂} {P : Set ℓ₁} {Q : Set ℓ₂} → (P → Q) → (¬ {ℓ₁Q → ℓ₂} {P : Set ℓ₁} {Q : Set ℓ₂} → (P → Q) → (¬ Q → ¬ P)
 contrapositive p→q ¬q p = ¬q (p→q p)
 {% endraw %}
@@ -454,360 +429,285 @@ Using the above, we can decide equality of two identifiers by deciding equality on the underlying strings. 
{% raw %}
-_≟_ : (x y : Id) → Dec (x ≡ y)
+id x ≟ id y with x Data.Nat.≟ y
+id →x Dec≟ (xid y ≡| y)yes refl  =  yes refl
 id x ≟ id y with x Data.String.≟| y
-id x ≟ idno  x≢y   = y |  no yes refl  =  yes refl
-id x ≟ id y | no  x≢y   =  no (contrapositive id-inj x≢y)
   where
     id-inj : ∀ {x y} → id x ≡ id y → x ≡ y
     id-inj refl  =  refl
 {% endraw %}
-We define some identifiers for future use. - -
{% raw %}
-x y z : Id
-x = id "x"
-y = id "y"
-z = id "z"
-{% endraw %}
- ## Total Maps Our main job in this chapter will be to build a definition of @@ -828,48 +728,48 @@ _total maps_ that return a default value when we look up a key that is not present in the map. 
{% raw %}
-TotalMap : Set → Set
 TotalMap A = Id → A
 {% endraw %}
@@ -878,15 +778,15 @@ 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 %}
-module TotalMap where
 {% endraw %}
@@ -896,64 +796,64 @@ default element; this map always returns the default element when applied to any id. 
{% raw %}
-  always : ∀ {A} → A → TotalMap A
   always v x = v
 {% endraw %}
@@ -963,176 +863,176 @@ 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 %}
-  infixl 15 _,_↦_  
 
   _,_↦_ : ∀ {A} → TotalMap A → Id → A → TotalMap A
   (ρ , x ↦ v) y with x ≟ y
   ... | yes x=yx≡y = v
   ... | no  x≠yx≢y = ρ y
 {% endraw %}
@@ -1145,69 +1045,273 @@ 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 %}
-  module example where
+
+    x y z : Id
+    x = id 0
+    y = id 1
+    z = id 2
+
+    ρ₀ : TotalMap ℕ
+    ρ₀ = always 0 , x ↦ 42 , y ↦ 69
+
+    test₁ : ρ₀ x ≡ 42
+    test₁ = : TotalMap ℕrefl
-  ρ₀test₂ : =ρ₀ alwaysy 0≡ , x ↦ 4269
+    test₂ ,= yrefl
+
+    test₃ ↦: 69ρ₀ z ≡ 0
+    test₃ = refl
 {% endraw %}
@@ -1215,123 +1319,6 @@ 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₁ : ρ₀ x ≡ 42
-  test₁ = refl
-
-  test₂ : ρ₀ y ≡ 69
-  test₂ = refl
-
-  test₃ : ρ₀ z ≡ 0
-  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 exercises, make sure you understand the statements of @@ -1341,184 +1328,184 @@ the lemmas! The `always` map returns its default element for all keys: 
{% raw %}
-  postulate
     apply-always : ∀ {A} (v : A) (x : Id) → always v x ≡ v
 {% endraw %}