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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Thu, 22 Apr 2021 19:49:07 +0200*Ironport-hdrordr*: A9a23:z+vXg6t00EtWQShLz05sRTHt7skD9tV00zAX/kB9WHVpW+afkN2jm+le8BfyhioYVn1Io6HmBICrR3TA+ZlppbQLNbC5UwX8/EeuJodu7YztqgeQfxHW3OhbyKtmbuxCGMT9ZGIK6PrSzQGkH78boeWv37uvgY7loEtFbQYvUK146hc8NwDzKDwVeCBjJb4UUKWR/dBGoT3IQwV1Uu2eCmMeV+bO4/3n/aiJXTc8CxQq6BaDgFqTgdaQLzGi0hgTSD9Jy7s5mFKoryXC+q6hv/unoyW360bv6f1t9efJ9sFOH4ilhMQTN1zX6jqVWA==*References*: <83feca0e-9080-4c90-b522-5a92f363dec7n@googlegroups.com>

Hello, although there is a standard module for real numbers in TLA+, neither TLC nor TLAPS support reasoning about real numbers at this point. Stephan
--
You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/45E91935-9CAF-42E6-9D7E-1C6C5758143F%40gmail.com. |

**References**:

- Prev by Date:
**[tlaplus] Floating Point operations to check equivalence of algorithms** - Next by Date:
**Re: [tlaplus] Floating Point operations to check equivalence of algorithms** - Previous by thread:
**[tlaplus] Floating Point operations to check equivalence of algorithms** - Next by thread:
**Re: [tlaplus] Floating Point operations to check equivalence of algorithms** - Index(es):