[Agda] "with .. postulate"

[Andreas Abel]

Sorry, I cannot explain this, because I cannot run your example 
(incomplete). --Andreas

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?
>
> Thanks,
>
> ------
> Sergei
>
>
>
> _______________________________________________
> 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/