From 020fed2395f44c5ae488abfaa6468af051dbdb59 Mon Sep 17 00:00:00 2001
From: wadler <wadler@inf.ed.ac.uk>
Date: Thu, 6 Jul 2017 23:12:06 +0100
Subject: [PATCH] tried out C-c C-a

---
 src/Stlc.lagda | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/Stlc.lagda b/src/Stlc.lagda
index d883ba74..c1aa58a0 100644
--- a/src/Stlc.lagda
+++ b/src/Stlc.lagda
@@ -117,7 +117,7 @@ data _⟹*_ : Term → Term → Set where
 reduction₁ : not · true ⟹* false
 reduction₁ =
     not · true
-  ⟹⟨ (β⇒ value-true) ⟩
+  ⟹⟨ β⇒ value-true ⟩
     if true then false else true
   ⟹⟨ β𝔹₁ ⟩
     false
@@ -218,4 +218,6 @@ that `var x`, `false`, and `true` are typed using `Ax`, `𝔹-I₂`, and
 that `(∅ , x ∶ 𝔹) x = just 𝔹`, which can in turn be specified with a
 hole. After filling in all holes, the term is as above.
 
+The entire process can be automated using Agsy, invoked with C-c C-a.
+