On Tue, Jan 25, 2005 at 05:49:10PM +0100, Sebastian Hanowski wrote:
> Why can't Epigram give me something like this for a case on l
> (manipulated):
>
> ------------------------------------------------------------------------
> ( l : List Nat !
> let !--------------!
> ! p l : * )
>
> p l <= case l
> { p nil []
> p (cons zero l) []
> p (cons (suc n) l) []
> }
> ------------------------------------------------------------------------
>
> To me it's obvious that if i'll specify which things i expect in a data
> structure, i intend to compute with them hence will inspect them. But
> the signature doesn't suffice to communicate this to the elaborator.
It is perhaps obvious that you intend to compute with them, but it isn't so
obvious how. Case analysis is just one thing you might want to do - you may
also for example want to call a helper function, or use a view. Admittedly,
this isn't likely to be the case with Nat, but with something more complex,
eliminating by case x is unlikely to be what you want.
Still, I look forward to the day when the UI lets me do case analysis with a
single keypress!
Edwin.
