[Agda] unsolved meta with abstraction example
rick
rick at rickmurphy.org
Wed Jul 4 04:05:18 CEST 2018
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
More information about the Agda
mailing list