[Agda] simple question

[Andrew Harris]

Hello,

   I am having trouble writing a simple function called lessThanEq.  It
takes two integers and should return a boolean "true" if the first is less
than or equal to the second.  I tried to write it like this:

open import Data.Bool
open import Data.Integer

module Test where

lessThanEq : ℤ → ℤ → Bool
lessThanEq x y = if (x ≤ y) then true else false

But Agda seems to tell me that the x ≤ y returns a Set instead of a Boolean
as in the following messages:

Set !=< Bool of type Set₁
when checking that the expression x ≤ y has type Bool

Am I doing something silly wrong or have I forgotten another standard
library that might help?

thanks,
-andrew
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150101/b8ee495b/attachment.html