[Agda] isYes

[Andreas Abel]

On 06.02.2014 16:17, Sergei Meshveliani wrote:
> I searched for  isYes, isYes?, yes?  in lib-0.7,
> and have discovered
>                      ⌊_⌋  in  module Relation.Nullary.Decidable.
>
> I wonder what is the origin of this denotation.

I do not know, but it certainly looks nice, e.g.

       if     ⌊ head (tail s) ≤? head (tail t) ⌋
       then   ihead p
       else   trans p₁ (ihead q)

Using some kind of brackets for this op certainly makes sense.

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Depeartment of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/