[Agda] type annotation in-place

[Sergei Meshveliani]

On Wed, 2015-10-07 at 14:34 +0200, Jesper Cockx wrote:
> I'm not sure if I understand. With _∋_, you could write
> 
> 
>         foo123foo = Foo ∋ foo'
>         
>         foo = Foo ∋ foo' (T ∋ f x) y
> 
> 
> You could also use a pattern synonym to put the type signature after
> the term instead of before:
> 
>         El : ∀ {a} (A : Set a) → A → A
>         El A x = x
>         
>         syntax El A x = x ∈ A
>  
>         foo123foo = foo' ∈ Foo
>         
>         foo = foo' (f x ∈ T) y ∈ Foo
>  


I see now. Thank you.
It works in many cases.
There remains the case of applying `abstract'.
For example:

-------------------------------------
El : ∀ {a} (A : Set a) → A → A
El A x = x

syntax El A x = x ∈: A

module ListOverSetoid {α α= : Level} (A : Setoid α α=)
  where
  ...
  _=set_ : Rel (List C) (α ⊔ α=)
  xs =set ys =  xs ⊆ ys × ys ⊆ xs

  abstract
    f = _=set_ ([] ∈: List C)    ∈: (List C → Set (α ⊔ α=))
-------------------------------------

The report is "Unsolved metas".
And without `abstract', it is type-checked.

Regards,

------
Sergei