[Agda] Failed type checking of standard lib after removed eta-contraction of function bodies in `Def.hs'

[Andreas Abel]

I undid my fix for issue 361, the library should compile again.

On 11/16/10 10:33 AM, Andreas Abel wrote:
>
>
> On 11/15/10 9:35 PM, Dirk Ullrich wrote:
>> Hi all,
>> when I try to generate all `agdai' files for the Agda standard lib at
>> once with the current Agda version from darcs repository I get an
>> error for `Data.Star.Decoration.agda':
>> ...
>> .../Data/Star/Decoration.agda:54,15-16
>> xs != ε of type Star (λ .i' .j → T .i' .j) j j
>> when checking that the pattern ε has type
>> Star (DecoratedWith (λ {.i} {.j} → P)) (nonEmpty xs) (nonEmpty ε)
>>
>> Here it is caused by Andreas' patch that removes eta-contraction of
>> function bodies in `Def.hs'.
>
> Seems plausible.
>
>> Can anyone reproduce this?
>
> If I had more main memory, probably...
>
> Andreas
>
>

-- 
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/