changed DeBruijn to Scoped
This commit is contained in:
parent
11e9a4e99d
commit
4e4fc99920
2 changed files with 10 additions and 6 deletions
2
index.md
2
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)
|
||||
|
|
|
@ -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)
|
Loading…
Reference in a new issue