[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