[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  
TLAPS.

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