<div dir="ltr"><div>I presume there are operations in the standard prelude to compute whether one natural is less than or equal to another with types</div><div><br></div><div>  Nat -> Nat -> Bool</div><div>  (n : Nat) -> (m : Nat) -> Dec (m \leq n)</div><div><br></div><div>But I can't find them. Where are they and what are they called? Cheers, -- P</div><div><br></div><div>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:</div><div><br></div><div>  Definitions about Nat</div><div><br></div><div>followed by nothing! I'm not sure why.</div><div><br></div><div> </div><div><br></div><br clear="all"><div><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div></div></div></div>
</div>