[Agda] record field as Instance Argument

[Chris Jenkins]

Guillermo,

Is there a particular reason you want A and EqA to be fields, instead of
parameters? If not, you can do:

open import Data.Bool
>
> record Eq (T : Set) : Set where
>   field
>     _==_ : (x y : T) → Bool
>
>   _/=_ : (x y : T) → Bool
>   x /= y = not (x == y)
> open Eq ⦃...⦄
>
> record A2 (A : Set) ⦃ EqA : Eq A ⦄ : Set where
>   field
>     a b : A
>
>   a≠b = a /= b
>


On Thu, Apr 23, 2015 at 10:38 AM, Guillermo Calderon - INCO <
calderon at fing.edu.uy> wrote:

> Hi,
>
> I am working with Instance Arguments to simulate Haskell classes
> as explained here:
>
>
> http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.InstanceArguments
>
> So, I have:
>
>  record Eq (t : Set) : Set where
>    field _==_ : t → t → Bool
>    _/=_ : t → t → Bool
>    a /= b = not $ a == b
>
> and the following record definition:
>
> record A2 : Set₁ where
>   field
>     A : Set
>     EqA : Eq A
>     a b : A
>   a≠b : Bool
>   a≠b =  a /= b
>
> Agda gives an error at the last /= :
> "No variable of type Eq A was found in scope".
> But EqA is in the scope.  Why Agda does not consider it?
>
> I can fix it defining an alias of EqA as an instance Eq.
> The keyword instance is required.
> I do not find the way to apply "instance" directly over the field EqA.
>
> record A2 : Set₁ where
>   field
>     A : Set
>     EqA : Eq A
>     a b : A
>   instance foo = EqA
>   a≠b : Bool
>   a≠b =  a /= b
>
> Is there a better  way to solve this?
> Thanks,
> Guillermo
>
>
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>



-- 
Christopher Jenkins
Embedded Systems Software Engineer
Genesi USA Inc.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150424/f19462d9/attachment.html