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.
Didn't Conor say he wanted to allow several gadgets on the same line? However, this wouldn't work for this example, since you only want to analyze the x in the 2nd case and you only know the name of the variable once you have done the first one.
T.
Sebastian Hanowski wrote:
* Thorsten Altenkirch [2005-01-25 17:16]:
I don't get this. Which case analysis do you have to do but you don't want to do?
I was argueing whether i didn't get 'enough' case analyis since the case analysis i get for l is the same as if i had declared l:List X .
-------------------------------------------------------------------- ( l : List Nat ! let !--------------! ! p l : * )
p l <= case l { p nil [] p (cons x l) [] } --------------------------------------------------------------------
Why do i have to do one more case analysis eventually? If i had wanted to write some generic code for lists i would not have instantiated its signature. Why is my explanation not effective enough to decompose my programs input in one go?
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.
I'm aware that what i ask for doesn't generalize nicely, since i
don't want to be forced to invent n answers for a single case on
some i:Fin n whose n has been is fixed. But for polymorphic types (Fin drops out, it's 'polyvalent'), do i
always have to start off with some code that's more generic than its
signature possibly says?
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.
