[Agda] Equality of arguments in Agda

[Nils Anders Danielsson]

On Mon, May 5, 2008 at 10:30 AM, Robert Rothenberg <robrwo at gmail.com> wrote:
>
> In Haskell, I can use the class system to define a function that works on
> any type with equality [...]

>  But I am unsure how to define such a function in Agda. As there is no class
> system, how do I specify it should be type with equality, and then use it in
> the function definition?

By passing suitable arguments or dictionaries directly to the function:

f : {a : Set} -> (a -> a -> Bool) -> ...

To simplify things you can use parameterised modules:

module M {a : Set} (_==_ : a -> a -> Bool) where
  ...

Or if you want to ensure that the function is a decidable equivalence relation:

open import Relation.Binary

module M (ds : DecSetoid) where
  open DecSetoid ds
  ...

>  Or if my only choice is to use something like if_then_else, then where is
> it defined in the standard library?

if_then_else_ is in Data.Bool. You can also use "with"
(http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Docs.MagicWith).

-- 
/NAD