Less restrictive --without-K [Re: [Agda] no longer type checks]

[Andreas Abel]

Thanks for checking!

I interpret that in this way that the previous criterion was a bit 
random, but the current criterion is too restrictive still.

Cheers,
Andreas

On 31.05.13 12:24 AM, Andrés Sicard-Ramírez wrote:
> On 30 May 2013 16:34, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
>> Q: Would it also check (without my patch) and this definition of equality?
>
> (I am missing a git branch)
>
>>
>> data _≡_ {A : Set} : A → A → Set where
>>    refl : ∀ {a} → a ≡ a
>>
>> Or would it check if you wrote zero == bla instead of bla == zero?
>
> In both cases the proof doesn't type check.
>
> Best,
>

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