[Agda] unsolved meta with abstraction example

[Ulf Norell]

I believe `p-nil` is to be understood as representing whatever proof you
would give when
proving a concrete property `P`, and not meant as a literal example. That
said, to fix the
yellow you need to provide the type argument A:

postulate p-nil : ∀ {A} -> P {A} []

/ Ulf

On Wed, Jul 4, 2018 at 4:05 AM, rick <rick at rickmurphy.org> wrote:

>
> First thanks for all the great work on Agda.
>
> There appears to be an unsolved meta in the with abstraction
> Generalization example here [1].
>
> Given
>
> postulate P : ∀{A} -> List A -> Set
>
> the property P is yellow in the p-nil postulate.
>
> postulate p-nil : P {!!}
>
> after only one step of refinement. It remains so in the next step P [].
>
> I am using release 2.5.3 and found no issues here [2].
>
> Could you please explain how to resolve?
>
> I am new to Agda, so I'm sure I've missed something.
>
> Thanks in advance.
>
>
> 1. http://agda.readthedocs.io/en/v2.5.2/language/with-abstraction.html
>
> 2. https://github.com/agda/agda/issues
>
>
> --
> rick
>
> --
> rick
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180704/b0815a8c/attachment.html>