From 5c02a1a5cbc330eca0ca44645069fb9e3ea67399 Mon Sep 17 00:00:00 2001 From: wadler Date: Thu, 29 Jun 2017 16:43:38 +0100 Subject: [PATCH] updated instructions in README --- README.md | 7 +- out/Maps.md | 4924 ++++++++++++------------- out/Stlc.md | 6627 +++++++++++++++------------------- out/StlcProp.md | 9197 +++++++++++++++++++++++------------------------ 4 files changed, 9975 insertions(+), 10780 deletions(-) diff --git a/README.md b/README.md index 9b39345c..f47fe6e5 100644 --- a/README.md +++ b/README.md @@ -6,10 +6,11 @@ permalink: /about/ How to host literal code. -In directory `sf/` run both the following in background: +In directory `sf/` the following: - $ jekyll serve & - $ watch make & + $ make clobber + $ make + $ make serve & The visible page appears at diff --git a/out/Maps.md b/out/Maps.md index 4d894678..9115afbd 100644 --- a/out/Maps.md +++ b/out/Maps.md @@ -968,171 +968,171 @@ takes `x` to `v` and takes every other key to whatever `ρ` does. > 10015 _,_↦_ _,_↦_ : ∀ {A} → TotalMap A → Id → A → TotalMap A (ρ , x ↦ v) y with x ≟ y ... | yes x=y = v ... | no x≠y = ρ y {% endraw %} @@ -1145,68 +1145,68 @@ 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 %}
-  ρ₀ : TotalMap ℕ
   ρ₀ = always 0 , x ↦ 42 , y ↦ 69
 {% endraw %}
@@ -1216,118 +1216,118 @@ 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 %}
@@ -1341,184 +1341,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 %}