<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div class="">The standard library defines synonyms that obscure the underlying types. I haven’t found C-c C-z to be of much use; I grep the source trees instead.</div><div class=""><br class=""></div><div class="">$ git grep Dec | grep Nat</div><div class="">src/Data/Nat/Base.agda:156:_≤?_ : Decidable _≤_</div><div class=""><br class=""></div><div class="">Here’s the second operation:</div><div class=""><a href="https://agda.github.io/agda-stdlib/Data.Nat.Base.html#3179" class="">https://agda.github.io/agda-stdlib/Data.Nat.Base.html#3179</a></div><div class=""><br class=""></div><div class="">We can obtain the first operation via projection:</div><div class=""><a href="https://agda.github.io/agda-stdlib/Relation.Nullary.Decidable.html#822" class="">https://agda.github.io/agda-stdlib/Relation.Nullary.Decidable.html#822</a></div><div class=""><br class=""></div><div class=""><br class=""></div><div class="">-- </div><div class="">M.</div><div class=""><br class=""></div><div class=""><br class=""></div><div class=""><br class=""><div><blockquote type="cite" class=""><div class="">On 15 Feb 2018, at 20:26, Philip Wadler <<a href="mailto:wadler@inf.ed.ac.uk" class="">wadler@inf.ed.ac.uk</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class=""><div class="">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 class=""><br class=""></div><div class=""> Nat -> Nat -> Bool</div><div class=""> (n : Nat) -> (m : Nat) -> Dec (m \leq n)</div><div class=""><br class=""></div><div class="">But I can't find them. Where are they and what are they called? Cheers, -- P</div><div class=""><br class=""></div><div class="">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 class=""><br class=""></div><div class=""> Definitions about Nat</div><div class=""><br class=""></div><div class="">followed by nothing! I'm not sure why.</div><div class=""><br class=""></div><div class=""> </div><div class=""><br class=""></div><br clear="all" class=""><div class=""><div class="gmail_signature"><div dir="ltr" class=""><div class=""><div dir="ltr" class="">. \ Philip Wadler, Professor of Theoretical Computer Science,<br class="">. /\ School of Informatics, University of Edinburgh<br class=""></div><div class="">. / \ and Senior Research Fellow, IOHK<br class=""></div><div dir="ltr" class="">. <span class=""><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank" class="">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div></div></div></div>
</div>
The University of Edinburgh is a charitable body, registered in<br class="">Scotland, with registration number SC005336.<br class="">_______________________________________________<br class="">Agda mailing list<br class=""><a href="mailto:Agda@lists.chalmers.se" class="">Agda@lists.chalmers.se</a><br class="">https://lists.chalmers.se/mailman/listinfo/agda<br class=""></div></blockquote></div><br class=""></div></body></html>