[Agda] Boolean and Decidable comparison

[Philip Wadler]

I presume there are operations in the standard prelude to compute whether
one natural is less than or equal to another with types

  Nat -> Nat -> Bool
  (n : Nat) -> (m : Nat) -> Dec (m \leq n)

But I can't find them. Where are they and what are they called? Cheers, -- P

PS. Using ^C ^Z to search Everything.agda (see previous thread) for Nat
Bool or Nat Dec yields nothing. Indeed, using it to search for Nat gives:

  Definitions about Nat

followed by nothing! I'm not sure why.




.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180215/232b7219/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180215/232b7219/attachment.ksh>