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)