[Agda] unsolved meta with abstraction example

[rick]

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

[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

Post by rick
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
https://lists.chalmers.se/mailman/listinfo/agda