[Agda] Puzzled about how instance arguments work in the presence of metas

Jesper Cockx Jesper at sikanda.be
Wed Oct 29 10:44:08 CET 2014


Can someone tell me if the code fragment below is supposed to work? It
gives me yellow, but it works fine when I replace `it` by the (unique)
solution `is-zero`.

it : {A : Set} {{_ : A}} → A
it {{x}} = x

data IsZero : Nat → Set where
  instance
    is-zero : IsZero 0

test : IsZero _
test = it

Cheers,
Jesper
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141029/0ab3e816/attachment.html


More information about the Agda mailing list