[Agda] type annotation in-place

[Nils Anders Danielsson]

On 2015-10-07 20:49, Sergei Meshveliani wrote:
>    abstract
>      f = _=set_ ([] ∈: List C)    ∈: (List C → Set (α ⊔ α=))
> -------------------------------------
>
> The report is "Unsolved metas".
> And without `abstract', it is type-checked.

If you use abstract, then meta-variables in the type signature are
frozen before the body is type-checked:

   https://github.com/agda/agda/issues/418

-- 
/NAD