[Agda] Re: A question on Setoid in the standard library

[David Leduc]

Dear myself,

You must add:

open import Relation.Nullary.Core
open Dec



On Wed, Sep 22, 2010 at 3:34 PM, David Leduc
<david.leduc6 at googlemail.com> wrote:
> I do not understand why the following code results in a parsing error.
> Please someone, help me.
>
> {-# OPTIONS --universe-polymorphism #-}
>
> module test where
>
> open import Level
> open import Relation.Binary
> open import Data.Bool
>
> f : (c l : Level)(A : DecSetoid c l) ->
>    DecSetoid.Carrier A -> DecSetoid.Carrier A -> Bool
> f c l A X Y with DecSetoid._≟_ A X Y
> ... | yes _ = true
> ... | no _ = true
>