[Agda] proofs and case-split

[Nils Anders Danielsson]

On 2009-09-23 11:52, Andreas Buechele wrote:
> For example the goal for the case next to last is
> 
> HoldsAll .P (proj₂ (joinˡ⁺ (1# , t₁) k₂ t₃ ∼+))
> 
> but I think it should be
> 
> Σ (.P k₂) (λ _ → Σ (HoldsAll .P t₁) (λ _ → HoldsAll .P t₃))
> 
> Why is that?

http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.PatternMatching

> Is there a smart solution for this problem?

The brute-force solution is to do further pattern matching on t₁ so that
the goal type evaluates.

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