<div dir="ltr"><div>Guillermo,<br><br></div>Is there a particular reason you want A and EqA to be fields, instead of parameters? If not, you can do:<br><br><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote"><font size="1"><span style="font-family:monospace,monospace">open import Data.Bool</span></font><br><font size="1"><span style="font-family:monospace,monospace"></span></font><br><font size="1"><span style="font-family:monospace,monospace">record Eq (T : Set) : Set where</span></font><br><font size="1"><span style="font-family:monospace,monospace"> field</span></font><br><font size="1"><span style="font-family:monospace,monospace"> _==_ : (x y : T) → Bool</span></font><br><font size="1"><span style="font-family:monospace,monospace"></span></font><br><font size="1"><span style="font-family:monospace,monospace"> _/=_ : (x y : T) → Bool</span></font><br><font size="1"><span style="font-family:monospace,monospace"> x /= y = not (x == y)</span></font><br><font size="1"><span style="font-family:monospace,monospace">open Eq ⦃...⦄</span></font><br><font size="1"><span style="font-family:monospace,monospace"></span></font><br><font size="1"><span style="font-family:monospace,monospace">record A2 (A : Set) ⦃ EqA : Eq A ⦄ : Set where</span></font><br><font size="1"><span style="font-family:monospace,monospace"> field</span></font><br><font size="1"><span style="font-family:monospace,monospace"> a b : A</span></font><br><font size="1"><span style="font-family:monospace,monospace"></span></font><br><font size="1"><span style="font-family:monospace,monospace"> a≠b = a /= b</span></font><br></blockquote><br></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Apr 23, 2015 at 10:38 AM, Guillermo Calderon - INCO <span dir="ltr"><<a href="mailto:calderon@fing.edu.uy" target="_blank">calderon@fing.edu.uy</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
I am working with Instance Arguments to simulate Haskell classes<br>
as explained here:<br>
<br>
<a href="http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.InstanceArguments" target="_blank">http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.InstanceArguments</a><br>
<br>
So, I have:<br>
<br>
record Eq (t : Set) : Set where<br>
field _==_ : t → t → Bool<br>
_/=_ : t → t → Bool<br>
a /= b = not $ a == b<br>
<br>
and the following record definition:<br>
<br>
record A2 : Set₁ where<br>
field<br>
A : Set<br>
EqA : Eq A<br>
a b : A<br>
a≠b : Bool<br>
a≠b = a /= b<br>
<br>
Agda gives an error at the last /= :<br>
"No variable of type Eq A was found in scope".<br>
But EqA is in the scope. Why Agda does not consider it?<br>
<br>
I can fix it defining an alias of EqA as an instance Eq.<br>
The keyword instance is required.<br>
I do not find the way to apply "instance" directly over the field EqA.<br>
<br>
record A2 : Set₁ where<br>
field<br>
A : Set<br>
EqA : Eq A<br>
a b : A<br>
instance foo = EqA<br>
a≠b : Bool<br>
a≠b = a /= b<br>
<br>
Is there a better way to solve this?<br>
Thanks,<br>
Guillermo<br>
<br>
<br>
<br>
<br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br><br clear="all"><br>-- <br><div class="gmail_signature"><div dir="ltr"><div><div>Christopher Jenkins<br></div>Embedded Systems Software Engineer<br></div>Genesi USA Inc.<br></div></div>
</div>