[Agda] isYes

[Nils Anders Danielsson]

On 2014-02-06 16:17, Sergei Meshveliani wrote:
> People,
>
> 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.

Brackets of this kind are sometimes used to denote various forms of
erasure.

-- 
/NAD