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

[Andrés Sicard-Ramírez]

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,
-- 
Andrés