[Agda] I'm having an issue modeling type classes with records
Andreas Abel
andreas.abel at ifi.lmu.de
Fri Sep 20 20:24:54 CEST 2013
On 20.09.2013 19:57, Chris Moline wrote:
>
> | module TypeClassModeling where
> |
> | data Bool : Set where
> | true false : Bool
> |
> | record Eq (t : Set) : Set where
> | field equal : t -> t -> Bool
> |
> | record Ord {a : Set} (A : Eq a) : Set where
> | field _<_ : A -> A -> Bool
This works:
record Ord {A : Set} (eq : Eq A) : Set where
field _<_ : A -> A -> Bool
less-than is still a relation on a *type* A!
--
Andreas Abel <>< Du bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
More information about the Agda
mailing list