[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