[Agda] "with .. postulate"

[Serge D. Mechveliani]

On Sun, Mar 03, 2013 at 08:25:44AM +0100, Andreas Abel wrote:
> Sorry, I cannot explain this, because I cannot run your example
> (incomplete). --Andreas
> 


    http://botik.ru/pub/local/Mechveliani/agdaNotes/rep.zip 

contains the precise  Main.agda  and  readme.agda
(please, read first  readme.agda).
I am sorry: the proggram is large.
I tried to present a small example, but have failed.
Of course, it can be reduced, say, 10 times, but this would need a 
considerable effort.
It looks like I am currently stuck in my attempt to write a library.

Thank you in advance for help,

-------
Sergei



> On 02.03.13 10:43 AM, Serge D. Mechveliani wrote:
> >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?
> >
> >
> >
> >_______________________________________________
> >Agda mailing list
> >Agda at lists.chalmers.se
> >https://lists.chalmers.se/mailman/listinfo/agda
> >
> 
> -- 
> Andreas Abel  <><      Du bist der geliebte Mensch.
> 
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
> 
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~abel/
>