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

Re: [tlaplus] Peano.tla

Le mercredi 8 juin 2016 14:01:32 UTC+2, Stephan Merz a écrit :

- I believe the requirement that successor be injective is missing in the Peano axioms as they are given in Specifying Systems, and I added it to the definition of natural numbers that underlies the Isabelle backend of  

Excuse me. I had misread the sentence. We agree. It is missing.