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

[Philip Wadler]

That worked perfectly!!! Thank you, Ulf! Cheers, -- P

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

On 28 February 2018 at 16:10, Ulf Norell <ulf.norell at gmail.com> wrote:

>
> 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/3f2d8398/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180228/3f2d8398/attachment.ksh>