[Agda] type annotation in-place

[Sergei Meshveliani]

On Wed, 2015-10-07 at 13:54 +0200, Jesper Cockx wrote:
> From Function.agda in the standard library:
> 
>         -- In Agda you cannot annotate every subexpression with a type
>         -- signature. This function can be used instead.
>         
>         _∋_ : ∀ {a} (A : Set a) → A → A
>         A ∋ x = x
> 
> 
> Does this solve your problem?
> 

No. I meant the implementation part -- the part after  `` = ''.

------
Sergei




> On Wed, Oct 7, 2015 at 1:41 PM, Sergei Meshveliani <mechvel at botik.ru>
> wrote:
>         Is it possible to allow in Language the syntax like
>         
>           foo123foo = foo' : Foo
>         
>         (instead of
>           foo123foo : Foo
>           foo123foo = foo'
>         )
>         ?
>         
>         And one also could think of expressions like
>         
>           foo = foo' (f x : T) y  : Foo
>         
>         This will make programs a bit more readable.
>         
>         Regards,
>         
>         ------
>         Sergei
>         
>         _______________________________________________
>         Agda mailing list
>         Agda at lists.chalmers.se
>         https://lists.chalmers.se/mailman/listinfo/agda
> 
>