* Thorsten Altenkirch [2005-01-26 13:38]:
> Sebastian Hanowski wrote:
> >* Thorsten Altenkirch [2005-01-25 18:30]:
> > > I see, you want iterated case analysis automatically.
> > >
> > > As Edwin points out, that's not always what you want. Maybe there
> > > should be a special gadget, case*, which iterates case analysis.
> >
> >
> > I'm in favor. Let's call it 'staircase to earth'. It takes patterns
> > to the ground.
>
> As Conor pointed out, my proposal is rather a "staircase to hell",
> since why should we stop at
>
> f nil
> f (cons 0 ns)
> f (cons (suc n) ns
>
> we can still analyze ns and n, why shouldn't we? And so on...
Don't case recursively. Do it only over variables of the type (Nat) to
which the polymorphic type constructor (List) is applied to.
> What we will be able to do is
>
> m,n : Nat
> let -----------
> f m n : Nat
>
> f m n <= case m n {
> f 0 0 []
> f 0 (suc n) []
> f (suc m) 0 []
> f (suc m) (suc n) []
> }
Just one more question: Would this be allowed to be handwritten or is it
the outcome of elaborating [<= case m n]?
Best regards,
Sebastian
