From b4f79811ca1949e9a025e74e887703b19ab4d32c Mon Sep 17 00:00:00 2001
From: wadler <wadler@inf.ed.ac.uk>
Date: Tue, 3 Apr 2018 20:57:07 -0300
Subject: [PATCH] coded up TypedDB

---
 Notes.md           | 19 ++++++++++++++++++-
 src/StlcProp.lagda |  2 --
 2 files changed, 18 insertions(+), 3 deletions(-)

diff --git a/Notes.md b/Notes.md
index 25a22c40..6798001f 100644
--- a/Notes.md
+++ b/Notes.md
@@ -29,7 +29,24 @@ The following comments were collected on the Agda mailing list.
 
 ## Untyped lambda calculus
 
-* http://www.cse.chalmers.se/~nad/listings/partiality-monad/Lambda.Simplified.Delay-monad.Interpreter.html
+* Nils Anders Danielsson <nad@cse.gu.se>
+  +
+  http://www.cse.chalmers.se/~nad/listings/partiality-monad/Lambda.Simplified.Delay-monad.Interpreter.html
+  + /~nad/repos/codata/Lambda/Closure/Functional
+* untyped lambda calculus by Gallais
+  + https://gist.github.com/gallais/303cfcfe053fbc63eb61
+* lambda calculus
+  + https://github.com/pi8027/lambda-calculus/tree/master/agda/Lambda
+
+## Agda resources
+* Chalmers class
+  + http://www.cse.chalmers.se/edu/year/2017/course/DAT140_Types/
+* Dybjer lecture notes
+  + http://www.cse.chalmers.se/edu/year/2017/course/DAT140_Types/LectureNotes.pdf
+* Ulf Norell and James Chapman lecture notes
+  + http://www.cse.chalmers.se/~ulfn/darcs/AFP08/LectureNotes/AgdaIntro.pdf
+* Chalmer Take Home exam 2017
+  + http://www.cse.chalmers.se/edu/year/2017/course/DAT140_Types/TakeHomeExamTypes2017.pdf
 
 ## Syntax for lambda calculus
 
diff --git a/src/StlcProp.lagda b/src/StlcProp.lagda
index 6e69fdbf..9c34ee99 100644
--- a/src/StlcProp.lagda
+++ b/src/StlcProp.lagda
@@ -161,10 +161,8 @@ substitution.  Working from top to bottom (from the high-level
 property we are actually interested in to the lowest-level
 technical lemmas), the story goes like this:
 
-  <!--
   - The _preservation theorem_ is proved by induction on a typing derivation.
     derivation, pretty much as we did in chapter [Types]({{ "Types" | relative_url }})
-  -->
 
   - The one case that is significantly different is the one for the
     `βλ·` rule, whose definition uses the substitution operation.  To see that