* Conor McBride [2005-01-26 13:38]: > Sebastian Hanowski wrote: > > * Thorsten Altenkirch [2005-01-25 18:30]: > > > 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. > > 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?
I can't answer this. See, partly my question was caused by the fact that - like you mentioned in the tutorial - for some i:Fin n case on n will just tell if there's a construction or not, but not which one. On the other hand, doesn't fixing n turn Fin n into an enumerated type? This is impractical, but why shouldn't give case on i the ground patterns for the inhabitants of its type (supposed its index is in normal form)? Best regards, Sebastian
