[Agda] simple question

[flicky frans]

Or just

  open import Relation.Nullary.Decidable using (⌊_⌋)
  open import Data.Bool using (Bool)
  open import Data.Integer using (ℤ; _≤?_)

  lessThanEq : ℤ → ℤ → Bool
  lessThanEq x y = ⌊ x ≤? y ⌋

2015-01-01 22:07 GMT+03:00, Sergei Meshveliani <mechvel at botik.ru>:
> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>