diff --git a/out/Stlc.md b/out/Stlc.md index 5d615dea..97120503 100644 --- a/out/Stlc.md +++ b/out/Stlc.md @@ -366,7 +366,7 @@ And here it is formalised in Agda. Terms have six constructs. Three are for the core lambda calculus: - * Variables, `\` x` + * Variables, `` ` x `` * Abstractions, `λ[ x ∶ A ] N` * Applications, `L · M` and three are for the base type, booleans: @@ -390,213 +390,213 @@ Here is the syntax of terms in BNF. 
 
-infixl 20 20 _·_
 infix  15 λ[_∶_]_
 infix  15 if_then_else_
 
 data Term : Set where
   ` : Id →Id → Term
   λ[_∶_]_ : Id →Id → Type → Term → Term
   _·_ : Term → Term → Term
   true : Term
   false : Term
   if_then_else_ : Term → Term → Term → Term
 
@@ -613,225 +613,225 @@ CONTINUE FROM HERE
 Example terms.
 
 
-f x : Id Id
 f  =  =  id 0
 x  =  =  id 1
 
 not two : Term 
 not =  λ[ x ∶ 𝔹 ] (if ` x then false else true)
 two =  λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ λ[ x ∶ 𝔹 ] ` f · (` f · (` f · ` x)
 
@@ -841,130 +841,130 @@ Example terms.
 
 
 
-data Value : Term → Set where
   value-λ     : ∀ {x A{x N}A → Value (λ[ x ∶ A ] N)} → Value (λ[ x ∶ A ] N)
   value-true  :  : Value true
   value-false : Value false
 
@@ -974,645 +974,645 @@ Example terms.
 
 
 
-_[_:=_] : Term → Id Id → Term → Term
 (` x′) [ x := V:= V ] with x ≟ x′ x′
 ... | yes _ = V
 ... | no  _ no  _ = ` x′ x′
 (λ[ x′ ∶x′ A′∶ A′ ] N′) [ x := := V ] with x ≟ x′ x′
 ... | yes _ = λ[ x′λ[ ∶x′ A′∶ ]A′ N′] N′
 ... | no  _ no  _ = λ[ x′λ[ ∶x′ A′∶ A′ ] (N′ [ x := V:= ])V ])
 (L′ · M′) [ x := V ] =  (L′ [ x := V ] =  (L′ [ x V:= ])V ]) · (M′ [ x := V:= ])V ])
 (true) [ x := := V ] = true
 (false) [ x := := V ] = false
 (if L′ thenL′ M′then M′ else N′) [ x := := V ] = if if (L′ [ x := V:= ])V ]) then (M′ [ x := V:= ])V ]) else (N′ [ x := V:= V ])
 
@@ -1622,569 +1622,569 @@ Example terms.
 
 
 
-infix 10 10 _⟹_ 
 
 data _⟹_ : Term → Term → Set where
   βλ· : ∀ {x {x A N V} → Value V} → Value V →
     (λ[ x ∶ A ] N) · V ⟹ N) · V ⟹ N [ x := V:= V ]
   ξ·₁ : ∀ {L L′{L M}L′ M} →
     L ⟹ L′ L′ →
     L · M ⟹ L′ ·L′ · M
   ξ·₂ : ∀ {V M M′} →
-    Value {V M M′} →
     Value V →
+    M ⟹ M′ M′ →
     V · M ⟹ V · M′ M′
   βif-true : ∀ {M N}{M N} →
     if true then M else N ⟹ M
   βif-false : ∀ {M N}{M N} →
     if false then M else N ⟹ N
   ξif : ∀ {L L′{L ML′ N}M N} →
     L ⟹ L′ L′ →    
     if L then M else N ⟹ if L′if L′ then M else N
 
@@ -2195,665 +2195,665 @@ Example terms.
 
 
 
-infix 10 10 _⟹*_ 
 infixr 2 _⟹⟨_⟩_
 infix  3 _∎  3 _∎
 
 data _⟹*_ : Term → Term → Set where
   _∎ : ∀ M → M ⟹* ⟹* M
   _⟹⟨_⟩_ : ∀ L {ML N}{M →N} → L ⟹ M → M ⟹* N → L ⟹* N → L ⟹* N  
 
 reduction₁ : not · true ⟹* ⟹* false
 reduction₁ =
     not · true
   ⟹⟨ βλ· value-true ⟩
     if true then false else true
   ⟹⟨ βif-true ⟩
     false
   ∎
 
 reduction₂ : two · not · true ⟹* ⟹* true
 reduction₂ =
     two · not · true
   ⟹⟨ ξ·₁ (βλ· value-λ) ⟩
     (λ[ x ∶ 𝔹 ] not · (not · ` x)) · true
   ⟹⟨ βλ· value-true ⟩
     not · (not · true)
   ⟹⟨ ξ·₂ value-λ (βλ· value-true) ⟩
     not · (if true then false else true)
   ⟹⟨ ξ·₂ value-λ βif-true  ⟩  ⟩
     not · false
   ⟹⟨ βλ· value-false ⟩
     if false then false else true
   ⟹⟨ βif-false ⟩
     true
   ∎
 
@@ -2867,683 +2867,683 @@ Much of the above, though not all, can be filled in using C-c C-r and C-c C-s.
 
 
 
-Context : Set
 Context = PartialMap Type
 
 infix 10 10 _⊢_∶_
 
 data _⊢_∶_ : Context → Term → Type → Set where
   Ax : ∀ {Γ x{Γ A}x A} →
     Γ x ≡ just A →
     Γ ⊢ ` x ∶ A
   ⇒-I : ∀ {Γ {Γ x N A B} →
-    Γ , x ∶ A ⊢ N ∶ B} →
     Γ , x ∶ A ⊢ λ[N ∶ B →
+    Γ ⊢ λ[ x ∶ A ] N ∶ A ⇒ B
   ⇒-E : ∀ {Γ {Γ L M A B} B} →
     Γ ⊢ L ∶ A ⇒ B →
     Γ ⊢ M ∶ A →
     Γ ⊢ L · M ∶ B
   𝔹-I₁ : ∀ {Γ} →
     Γ ⊢ true ∶ 𝔹
   𝔹-I₂ : ∀ {Γ} →
     Γ ⊢ false ∶ 𝔹
   𝔹-E : ∀ {Γ {Γ L M N A} A} →
     Γ ⊢ L ∶ 𝔹 →
     Γ ⊢ M ∶ A →
     Γ ⊢ N ∶ A →
     Γ ⊢ if if L then M else N ∶ A
 
@@ -3553,205 +3553,205 @@ Much of the above, though not all, can be filled in using C-c C-r and C-c C-s.
 
 
 
-typing₁ : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹
 typing₁ = ⇒-I (𝔹-E (Ax refl) 𝔹-I₂ 𝔹-I₁)
 
 typing₂ : ∅ ⊢ two ∶ (𝔹 ⇒ (𝔹) ⇒ ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹
 typing₂ = ⇒-I (⇒-I (⇒-E (Ax refl) (⇒-E (Ax refl) (Ax refl))))
 
@@ -3785,7 +3785,7 @@ outermost term is now `if_then_else_`, which is typed using `𝔹-E`. The
     ?2 : ∅ , x ∶ 𝔹 ⊢ true ∶ 𝔹
 
 Again we fill in the three holes by typing C-c C-r in each. Agda observes
-that `\` x`, `false`, and `true` are typed using `Ax`, `𝔹-I₂`, and
+that `` ` x ``, `false`, and `true` are typed using `Ax`, `𝔹-I₂`, and
 `𝔹-I₁` respectively. The `Ax` rule in turn takes an argument, to show
 that `(∅ , x ∶ 𝔹) x = just 𝔹`, which can in turn be specified with a
 hole. After filling in all holes, the term is as above.
diff --git a/out/StlcProp.md b/out/StlcProp.md
index 54616b83..86a1c3bc 100644
--- a/out/StlcProp.md
+++ b/out/StlcProp.md
@@ -433,7 +433,7 @@ while for boolean types they are values `true` and `false`.
       >: Term → Type  (λ[ x ∶ A ] A ⇒ canonical true for 𝔹
@@ -584,7 +584,7 @@ while for boolean types they are values `true` and `false`.
       >canonical false for 𝔹
@@ -630,7 +630,7 @@ while for boolean types they are values `true` and `false`.
       >∅ ⊢ L ∶ → Value  (Ax  (⇒-I ) value-λ  (⇒-E canonical-forms 𝔹-I₁ value-true canonical-forms 𝔹-I₂ value-false  (𝔹-E : Term M ⟹ → Value ∅ ⊢ M ∶  (Ax  (⇒-I done value-λ
@@ -1123,7 +1123,7 @@ This completes the proof.
       > (⇒-E  (ξ·₁  (ξ·₂  (βλ· progress 𝔹-I₁ done value-true
@@ -1348,7 +1348,7 @@ This completes the proof.
       >progress 𝔹-I₂ done value-false
@@ -1371,7 +1371,7 @@ This completes the proof.
       > (𝔹-E  (ξif steps βif-true
@@ -1517,7 +1517,7 @@ This completes the proof.
       >steps βif-false
 
@@ -1575,7 +1575,7 @@ instead of induction on typing derivations.
       >∅ ⊢ M ∶ → Term ∈ `  (λ[ y ∶ A ] L · L ·  (if L then M else  (if L then M else  (if L then M else → Term : Term : f ≢ x
@@ -2435,7 +2435,7 @@ Here are proofs corresponding to the first two examples above.
       >: x  (λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x): f  (λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x): x  ((λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x) · ` f): f  ((λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x) · ` f): x  (λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] ` f · ` x): f  (λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] ` f · ` x)Γ ⊢ M ∶ 
 
-free-lemma free-` (Ax Γx≡A) = (_ , Γx≡A) = (_ , Γx≡A)
 free-lemma (free-·₁ x∈L) (⇒-E ⊢L ⊢M) = ⊢M) = free-lemma x∈L ⊢L
 free-lemma (free-·₂ x∈M) (⇒-E ⊢L ⊢M) = free-lemma x∈M ⊢M) = free-lemma x∈M ⊢M
 free-lemma (free-if₁ x∈L) (𝔹-E ⊢L ⊢M ⊢N)⊢L =⊢M ⊢N) = free-lemma x∈L ⊢L
 free-lemma (free-if₂ x∈M) (𝔹-E ⊢L ⊢M ⊢N)⊢L =⊢M ⊢N) = free-lemma x∈M ⊢M
 free-lemma (free-if₃ x∈N) (𝔹-E ⊢L ⊢M ⊢N)⊢L =⊢M free-lemma x∈N ⊢N) = free-lemma x∈N ⊢N
 free-lemma (free-λ {x} {y} y≢x x∈N) (⇒-I ⊢N) with free-lemma x∈N ⊢N
-... | Γx≡C with y ≟ {x} {y} y≢x x∈N) (⇒-I ⊢N) with free-lemma x∈N ⊢N
 ... | Γx≡C with y ≟ |x yes y≡x = ⊥-elim (y≢x y≡x)
 ... | no  _   yes y≡x = ⊥-elim (y≢x y≡x)
+... | no  _   = Γx≡C
 
@@ -3629,68 +3629,68 @@ typed in the empty context is closed (has no free variables).
 
 
 
-postulate
   ∅⊢-closed : ∀ {M A}∀ →{M ∅ ⊢A} M→ ∶∅ A⊢ →M closed∶ A → closed M
 
@@ -3699,294 +3699,294 @@ typed in the empty context is closed (has no free variables).