[Agda] trouble with "with"

[Nils Anders Danielsson]

On 2008-12-29 15:02, Thorsten Altenkirch wrote:
>
> However, I got badly stuck on a with pattern. Agda tells me that it 
> "Cannot split on the constructor vapp".

Your code forces Agda to perform a case split on the second component of
the pair before splitting the result of the with expression. If you dot
the ε pattern, then the code type checks:

   spAppV : ∀ {Γ σ τ} (ts : Sp Γ σ τ) → SpAppV ts
   spAppV ε        = vε
   spAppV (t , ts) with spAppV ts
   spAppV (t , .ε)             | vε         = vapp ε t
   spAppV (t , .(appSp ts t')) | vapp ts t' = vapp (t , ts) t'

If you had used case-split (C-c C-c), then this dotting would have been
performed automatically. (Unfortunately the output of case-split is not
proper Agda code in this case.)

-- 
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.