<div dir="ltr">Hello,<div><br></div><div>   I am having trouble writing a simple function called lessThanEq.  It takes two integers and should return a boolean &quot;true&quot; if the first is less than or equal to the second.  I tried to write it like this:</div><div><br></div><div><div>open import Data.Bool</div><div>open import Data.Integer</div><div><br></div><div>module Test where</div><div><br></div><div>lessThanEq : ℤ → ℤ → Bool</div><div>lessThanEq x y = if (x ≤ y) then true else false</div></div><div><br></div><div>But Agda seems to tell me that the x ≤ y returns a Set instead of a Boolean as in the following messages:</div><div><br></div><div><div>Set !=&lt; Bool of type Set₁</div><div>when checking that the expression x ≤ y has type Bool</div></div><div><br></div><div>Am I doing something silly wrong or have I forgotten another standard library that might help?</div><div><br></div><div>thanks,</div><div>-andrew</div></div>