[Epigram] Re: a case for star

[Thorsten Altenkirch]

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...
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) []
        }
Cheers,
Thorsten


Sebastian
--
Dr. Thorsten Altenkirch            phone : (+44) (0)115 84 66516
Lecturer                           http://www.cs.nott.ac.uk/~txa/
School of Computer Science & IT        University of Nottingham
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.