From b0a6f9bc5a5badad9f63a48aae9224869800d6ef Mon Sep 17 00:00:00 2001 From: Philip Wadler Date: Mon, 17 Jul 2017 18:12:41 +0100 Subject: [PATCH] small fix to Stlc --- out/Stlc.md | 256 ++++++++++++++++++++++++------------------------- src/Stlc.lagda | 2 +- 2 files changed, 129 insertions(+), 129 deletions(-) diff --git a/out/Stlc.md b/out/Stlc.md index 42ef35ef..d2b6f035 100644 --- a/out/Stlc.md +++ b/out/Stlc.md @@ -5313,7 +5313,7 @@ Here are the above derivations formalised in Agda. -## Interaction with Agda +#### Interaction with Agda Construction of a type derivation is best done interactively. Start with the declaration: @@ -5359,245 +5359,245 @@ In other words, no type `A` is the type of this term. 
 
-contradiction : ∀: ∀ {A B}A B→} ¬→ (𝔹¬ ≡(𝔹 A≡ ⇒A ⇒ B)
 contradiction ()
 
 notyping : ∀: {A}∀ {A→} ¬→ (∅¬ ⊢(∅ λ[⊢ xλ[ ∶x 𝔹∶ ]𝔹 λ[] yλ[ ∶y 𝔹∶ ]𝔹 `] x` ·x `· y` ∶y ∶ A)
 notyping (⇒-I (⇒-I (⇒-E (Ax Γx) ) (Ax Γy)))) = =  contradiction (just-injective Γx)
 
diff --git a/src/Stlc.lagda b/src/Stlc.lagda
index 2c7484d8..e4f4ae05 100644
--- a/src/Stlc.lagda
+++ b/src/Stlc.lagda
@@ -779,7 +779,7 @@ typing₂ : ∅ ⊢ two ∶ (𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹
 typing₂ = ⇒-I (⇒-I (⇒-E (Ax refl) (⇒-E (Ax refl) (Ax refl))))
 \end{code}
 
-## Interaction with Agda
+#### Interaction with Agda
 
 Construction of a type derivation is best done interactively.
 Start with the declaration: