From a43bdb46c776cf183181c9a50f3702e1aa15da52 Mon Sep 17 00:00:00 2001 From: Philip Wadler Date: Fri, 14 Jul 2017 10:56:59 +0100 Subject: [PATCH] fixed backticks in code spans --- out/Stlc.md | 3586 +++++++++++++------------- out/StlcProp.md | 6108 ++++++++++++++++++++++---------------------- src/Stlc.lagda | 4 +- src/StlcProp.lagda | 4 +- 4 files changed, 4851 insertions(+), 4851 deletions(-) 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).