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

[Andreas Abel]

The error message is confusing:

The indices
   x ∷ xs
are not constructors (or literals) applied to variables (note that
parameters count as constructor arguments)

First, it uses plural for a single index (I am changing this right now). 
  Further, it is not a true statement, because x :: xs  _is_ a 
constructor applied to variables.  Whatever it wants to tell me, I do 
not get it.

On 29.05.13 8:59 PM, Nils Anders Danielsson 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
>
>

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