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.
When does it stop? How should case* choose which things to expand and which
not? It's not a trick question. I can think of at least one vaguely sensible
strategy which such a thing might adopt.
So tell me this, how would you calculate the type and definition of the
elimination operator case* from the definition of the datatype over which it
operates? If you can't tell me that, then there's no way to make it a
primitive notion. But if you can tell me that, perhaps it's a derivable
notion...
Cheers
Conor
--
http://www.cs.nott.ac.uk/~ctm
