[Agda] 3 newbie's questions, sorry!

[gallais at EnsL]

Hi David,

The propositional equality _≡_ is defined in
Relation.Binary.PropositionalEquality. To encode negation, logical or
& and, I use ⊥ (Data.Empty), ⊎ (Data.Sum) and Σ (Data.Product).

To talk about decidability in agda, you might want to use Dec
(Relation.Nullary). Here is the translation of your Coq statement:

------------------------
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Nat

-- translation of "forall (A:Set), (forall (x y:A), {x=y}+{x<>y}) -> nat"

foo : ∀ {A : Set} →  (∀ (x y : A) → Dec (x ≡ y)) → ℕ
foo = {!!}
------------------------

Cheers,

--
guillaume



On 22 September 2010 14:45, David Leduc <david.leduc6 at googlemail.com> wrote:
> 1. In the standard library I cannot fine equality, negation, logical
> or, logical and...
> Where are they?
>
> 2. How can I translate in Agda the following Coq type?
>
>  forall (A:Set), (forall (x y:A), {x=y}+{x<>y}) -> nat
>
>
> 3. How do you deal with proof irrelevance in Agda?
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>