[Agda] 3 newbie's questions, sorry!

[Nils Anders Danielsson]

On 2010-09-22 13:18, gallais @ EnsL wrote:
> The propositional equality _≡_ is defined in
> Relation.Binary.PropositionalEquality. To encode negation, logical or
> &  and, I use ⊥ (Data.Empty), ⊎ (Data.Sum) and Σ (Data.Product).

Relation.Nullary.¬_ encodes negation.

> To talk about decidability in agda, you might want to use Dec
> (Relation.Nullary).

The modules mentioned above are all listed in the README (with links to
the modules' source code):

   http://www.cs.nott.ac.uk/~nad/listings/lib-0.3/README.html

--
/NAD