[Agda] trouble with "with"

[Thorsten Altenkirch]

Hi Nisse,

thanks a lot. It now seems rather obvious... :-}

Does C-c C-c work for with as well?

Cheers,
Thorsten

On 29 Dec 2008, at 14:36, Nils Anders Danielsson wrote:

> 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.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


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.