[Agda] Upcoming feature: Postfix projections

[Andreas Abel]

Hello Agda crowd,

I am implementing postfix projections

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

as discussed at the last Agda meeting in Glasgow.  Example:

   record Stream (A : Set) : Set where
     coinductive
     field head : A
           tail : Stream A
   open Stream

   zipWith : ∀{A B C} (f : A → B → C) (s : Stream A) (t : Stream B) → 
Stream C
   zipWith f s t .head = f (s .head) (t .head)
   zipWith f s t .tail = zipWith f (s .tail) (t .tail)

By default, result splitting (C-c C-c RET) will now introduce postfix 
projection copatterns rather than prefix projection copatterns as before.

The new notation is a bit similar to object oriented style, now you can 
write

   object .method arg1 ... argn

instead of

   method object arg1 ... argn

This new feature is available on github branch

   postfix-projections

Please give it some testing (and me some feedback) before I merge it 
into stable.

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/