<div dir="ltr">That worked perfectly!!! Thank you, Ulf! Cheers, -- P</div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div></div></div></div>
<br><div class="gmail_quote">On 28 February 2018 at 16:10, Ulf Norell <span dir="ltr"><<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><br><div class="gmail_extra"><div class="gmail_quote"><span class="">On Wed, Feb 28, 2018 at 2:31 PM, Roman <span dir="ltr"><<a href="mailto:effectfully@gmail.com" target="_blank">effectfully@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">The downside is that `agda-prelude` is not compatible with the standard library.</blockquote><div><br></div></span><div>These days agda-prelude is compatible with the standard library. The only wrinkle<br></div><div>is that the deriving Eq functionality gives you an implementation of the agda-prelude<br></div><div>Eq record, but converting it to the standard library equivalent should be straight-forward.<br><br></div><div>In fact here's the code:<br><br></div><div>\begin{code}<br></div><div>-- These two imports are from agda-prelude (<a href="https://github.com/UlfNorell/agda-prelude" target="_blank">https://github.com/UlfNorell/<wbr>agda-prelude</a>)<br></div><div>open import Tactic.Deriving.Eq using (deriveEq)<br>import Prelude<br><br>instance<br>  unquoteDecl EqType = deriveEq EqType (quote Type)<br>  unquoteDecl EqEnv  = deriveEq EqEnv  (quote Env)<br><br>⊥To⊥ : Prelude.⊥ → ⊥<br>⊥To⊥ ()<br><br>decToDec : ∀ {a} {A : Set a} → Prelude.Dec A → Dec A<br>decToDec (Prelude.yes x) = yes x<br>decToDec (Prelude.no nx) = no (⊥To⊥ ∘ nx)<span class=""><br><br>_≟T_ : ∀ (A B : Type) → Dec (A ≡ B)<br></span>A ≟T B = decToDec (A Prelude.== B)<span class=""><br><br>_≟_ : ∀ (Γ Δ : Env) → Dec (Γ ≡ Δ)<br></span>Γ ≟ Δ = decToDec (Γ Prelude.== Δ)<br></div><div>\end{code}<span class="HOEnZb"><font color="#888888"><br></font></span></div><span class="HOEnZb"><font color="#888888"><div><br></div><div>/ Ulf<br></div></font></span></div></div></div>
</blockquote></div><br></div>