From f949776082bdc4f99d4fa8fb9ac0a3482ba5843b Mon Sep 17 00:00:00 2001
From: Philip Wadler <wadler@inf.ed.ac.uk>
Date: Fri, 14 Jul 2017 11:26:50 +0100
Subject: [PATCH] syntax examples

---
 src/Stlc.lagda | 36 ++++++++++++++++++++++++++++++++++--
 1 file changed, 34 insertions(+), 2 deletions(-)

diff --git a/src/Stlc.lagda b/src/Stlc.lagda
index 05695f81..da75264e 100644
--- a/src/Stlc.lagda
+++ b/src/Stlc.lagda
@@ -113,11 +113,18 @@ data Term : Set where
   if_then_else_ : Term → Term → Term → Term
 \end{code}
 
-CONTINUE FROM HERE
+A NOTE ON : AND ∶
+
+USE OF ` FOR var
 
 
 
-Example terms.
+
+Here are a couple of example terms, `not` of type
+`𝔹 ⇒ 𝔹`, which complements its argument, and `two` of type
+`(𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹` which takes a function and a boolean
+and applies the function to the boolean twice.
+
 \begin{code}
 f x : Id
 f  =  id 0
@@ -128,6 +135,31 @@ not =  λ[ x ∶ 𝔹 ] (if ` x then false else true)
 two =  λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x)
 \end{code}
 
+As in Agda, functions of two or more arguments are represented via
+currying. This is made more convenient by declaring `_⇒_` to
+associate to the right and `_·_` to associate to the left.
+Thus,
+
+  `(𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹` abbreviates `(𝔹 ⇒ 𝔹) ⇒ (𝔹 ⇒ 𝔹)`,
+
+and similarly,
+
+  `two · not · true` abbreviates `(two · not) · true`.
+
+SCOPE OF λ OR if
+
+\begin{code}
+example₁ : (𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹 ≡ (𝔹 ⇒ 𝔹) ⇒ (𝔹 ⇒ 𝔹)
+example₁ = refl
+
+example₂ : two · not · true ≡ (two · not) · true
+example₂ = refl
+
+example₃ : λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x) ≡ (λ[ f ∶ 𝔹 ⇒ 𝔹 ] (λ[ x ∶ 𝔹 ] (` f · (` f · ` x))))
+example₃ = refl
+\end{code}
+
+
 ## Values
 
 \begin{code}