[Agda] Typed DeBruijn, typed Phoas, and untyped DeBruijn

[Ulf Norell]

On Wed, Feb 28, 2018 at 2:31 PM, Roman <effectfully at gmail.com> wrote:

> The downside is that `agda-prelude` is not compatible with the standard
> library.


These days agda-prelude is compatible with the standard library. The only
wrinkle
is that the deriving Eq functionality gives you an implementation of the
agda-prelude
Eq record, but converting it to the standard library equivalent should be
straight-forward.

In fact here's the code:

\begin{code}
-- These two imports are from agda-prelude (
https://github.com/UlfNorell/agda-prelude)
open import Tactic.Deriving.Eq using (deriveEq)
import Prelude

instance
  unquoteDecl EqType = deriveEq EqType (quote Type)
  unquoteDecl EqEnv  = deriveEq EqEnv  (quote Env)

⊥To⊥ : Prelude.⊥ → ⊥
⊥To⊥ ()

decToDec : ∀ {a} {A : Set a} → Prelude.Dec A → Dec A
decToDec (Prelude.yes x) = yes x
decToDec (Prelude.no nx) = no (⊥To⊥ ∘ nx)

_≟T_ : ∀ (A B : Type) → Dec (A ≡ B)
A ≟T B = decToDec (A Prelude.== B)

_≟_ : ∀ (Γ Δ : Env) → Dec (Γ ≡ Δ)
Γ ≟ Δ = decToDec (Γ Prelude.== Δ)
\end{code}

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180228/eab79aea/attachment.html>