From afcbb50b39687c3102b33de7344cd5374b61e29e Mon Sep 17 00:00:00 2001
From: Icelandjack <baldurpet@gmail.com>
Date: Thu, 14 Jul 2016 16:53:25 +0000
Subject: [PATCH] PVar needed to compile

```haskell
phoasExample :: Phoas v (x -> y -> x)
phoasExample = PLam (\x -> PLam (\y -> PVar x))
```

instead of

```haskell
phoasExample :: Phoas v (x -> y -> x)
phoasExample = PLam (\x -> PLam (\y -> x))
```
---
 paper.lhs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/paper.lhs b/paper.lhs
index afced79..fcf77f3 100644
--- a/paper.lhs
+++ b/paper.lhs
@@ -665,7 +665,7 @@ The reading of the type parameter |v| is the type of \emph{variables}.
 For example, the lambda term |(\x y -> x)| can be constructed as follows:
 \begin{code}
 phoasExample :: Phoas v (x -> y -> x)
-phoasExample = PLam (\x -> PLam (\y -> x))
+phoasExample = PLam (\x -> PLam (\y -> PVar x))
 \end{code}
 An attractive property of parametric \hoas{} is that we use Haskell binding to construct syntax, and that terms of type |(forall v. Phoas v a)| are always well-scoped \cite{phoas}.