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

[Nils Anders Danielsson]

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

-- 
/NAD