TLAPM syntax parser does not support bitfield number formats

tlaplus / tlapm

The TLA Proof Manager

https://proofs.tlapl.us/

BSD 2-Clause "Simplified" License

67 stars 20 forks source link

Open ahelwer opened 3 weeks ago

ahelwer commented 3 weeks ago

The following will fail:

---- MODULE Test ----
op == \b01010101
op == \B10101010
op == \o01234567
op == \O76543210
op == \h0123456789abcdef
op == \H9876543210FEDCBA
====

Bitfield number formats were put forward as a candidate for removal from the language in The Future of TLA+ [pdf].

Ref #159