From 4e4fc99920637eafdb3b7b59b7d64edfd3673654 Mon Sep 17 00:00:00 2001
From: wadler <wadler@inf.ed.ac.uk>
Date: Tue, 27 Feb 2018 14:50:21 +0100
Subject: [PATCH] changed DeBruijn to Scoped

---
 index.md                             |  2 +-
 src/{DeBruijn.lagda => Scoped.lagda} | 14 +++++++++-----
 2 files changed, 10 insertions(+), 6 deletions(-)
 rename src/{DeBruijn.lagda => Scoped.lagda} (98%)

diff --git a/index.md b/index.md
index 6c514a70..7d46da7e 100644
--- a/index.md
+++ b/index.md
@@ -40,4 +40,4 @@ http://homepages.inf.ed.ac.uk/wadler/
   - [Maps: Total and Partial Maps](Maps)
   - [Stlc: The Simply Typed Lambda-Calculus](Stlc)
   - [StlcProp: Properties of STLC](StlcProp)
-  - [DeBruijn: Scoped and Typed DeBruijn representation](DeBruijn)
+  - [Scoped: Scoped and Typed DeBruijn representation](Scoped)
diff --git a/src/DeBruijn.lagda b/src/Scoped.lagda
similarity index 98%
rename from src/DeBruijn.lagda
rename to src/Scoped.lagda
index 8df6ab62..8395ffdc 100644
--- a/src/DeBruijn.lagda
+++ b/src/Scoped.lagda
@@ -1,11 +1,15 @@
-## DeBruijn encodings in Agda
-
-\begin{code}
-module DeBruijn where
-\end{code}
+---
+title     : "Scoped: Scoped and Typed DeBruijn representation"
+layout    : page
+permalink : /Scoped
+---
 
 ## Imports
 
+\begin{code}
+module Typed where
+\end{code}
+
 \begin{code}
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; sym; trans; cong)