[Agda] simple question

[Sergei Meshveliani]

On Thu, 2015-01-01 at 13:51 -0500, Andrew Harris wrote:
> [..]
> 
> lessThanEq : ℤ → ℤ → Bool
> lessThanEq x y = if (x ≤ y) then true else false
> 
> [..]

Indeed,  x ≤ y  returns the set of witnesses for the relation  x ≤ y.
Your goal can be programmed, for example, as

------------------------------------------
open import Function using (case_of_)
open import Relation.Nullary using (yes)
open import Data.Integer using (ℤ; _≤?_)
open import Data.Bool using (Bool; true; false)

lessThanEq : ℤ → ℤ → Bool
lessThanEq x y = case x ≤? y of \ { (yes _) → true
                                  ; _       → false }
--------------------------------------------------------

Regards, 

------
Sergei