[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Enumeration types




Malcolm:
  I don't think you're doing anything wrong.
Logically, it doesn't make a difference whether you have
........
  |--------
[1]   emptyT?(x)
[2]   zeroT?(x)

or
[-1]  succT?(x)
  |--------
........

The simplifier treats them the same.  If you prefer the latter
form, I can see if there something I can do.  Please send me enough
information so that I can recreate your proof.

-Shankar