[Agda] "with .. postulate"

[Serge D. Mechveliani]

Dear all,
the attachement  t.agda.zip  

contains a small code example where the same declaration of kind
                                        postulate p : <signature>
is taken in   Agda-2.3.2 MAlonzo  
as a correct type for  p  or not  -- depending on whether  p  is set 
directly after ` = ' or in the last branch for `with'.

Can you, please, explain this?

Thanks,

------
Sergei
-------------- next part --------------
A non-text attachment was scrubbed...
Name: t.agda.zip
Type: application/zip
Size: 610 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20130302/d662f0f2/t.agda.zip