[Agda] Boolean and Decidable comparison

[Miëtek Bak]

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.

$ git grep Dec | grep Nat
src/Data/Nat/Base.agda:156:_≤?_ : Decidable _≤_

Here’s the second operation:
https://agda.github.io/agda-stdlib/Data.Nat.Base.html#3179

We can obtain the first operation via projection:
https://agda.github.io/agda-stdlib/Relation.Nullary.Decidable.html#822


-- 
M.



> On 15 Feb 2018, at 20:26, Philip Wadler <wadler at inf.ed.ac.uk> wrote:
> 
> 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/ <http://homepages.inf.ed.ac.uk/wadler/>The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180215/d36d06f4/attachment.html>