[Agda] --without-K option too restrictive?

[Andrés Sicard-Ramírez]

On 29 May 2013 13:59, Nils Anders Danielsson <nad at cse.gu.se> wrote:
> On 2013-05-29 17:26, Andrés Sicard-Ramírez wrote:
>>
>> Why the --without-K option rejects the following proof
>>
>> foo : {A : Set}(xs ys : List A) → P xs ys → Q xs ys
>> foo xs .(x ∷ xs) (x , refl) = helper x xs
>>
>> if I can prove foo using only subst
>>
>> foo' : {A : Set}(xs ys : List A) → P xs ys → Q xs ys
>> foo' xs ys (x , h) =
>>    subst (λ ys' → length xs < length ys') (sym h) (helper x xs)
>>
>> ?
>
>
> The --without-K flag is documented in the release notes of Agda 2.3.2:
>
>
> http://wiki.portal.chalmers.se/agda/uploads/Main.Download/release-notes-2-3-2.txt
>

Thanks. I understand why my proof was rejected, but it seems the
--without-K option is not only rejecting the axiom K, but the axiom K plus
something else.

-- 
Andrés