[isabelle-dev] Suc 0 necessary?

Amine Chaieb ac638 at cam.ac.uk
Mon Feb 23 16:48:28 CET 2009

Tobias Nipkow wrote:
> This is exactly the point: recursive functions defined by pattern 
> matching expect Suc. They tend to dominate the scene in CS-oriented 
> applications. Hence Suc 0 is made the default. However, for math 
> applications this tends to be inconvenient, esp in connection with 
> abstract algebra involving 1.

I never understood this argument completely. This solves the issue for 
1, but not for e.g. 2 , 3, 4 etc, where we must add nat_number or do 
something else if that is too dangerous. Isn't that so?


More information about the isabelle-dev mailing list