Karolis Petrauskas
Karolis Petrauskas
The duplicate #text elements were generated in the case, when xsd:extension was used for xsd:simpleContent. That was causing the generated records being invalid. We solve this by filter the duplicate...
Similarly, x.plus(y) is a shorthand for num.**next -> plus**(x,y)
This is related to https://github.com/tlaplus/tlapm/pull/93. The extension could suggest a user download and install the proper version of the TLAPS/LSP. We should return to this when the LSP support in...
- Fixed the way the stack traces are retrieved. - Also, I dropped the backward compatibility for namespaced types. It complicates usage under the ErlangLS. Not sure, if such non-backward-compatible...
It seems now that the `hamcrest.hrl` file is only generated to have all the matchers auto-imported. Would you accept a pull-request for making that header static or for replacing the...
Maybe it would be easier to integrate different changes if TLAPM had a `develop` branch along with the `master` (or `main`)? In such a case, all the pull requests should...
E.g. "Recursive operators not supported by TLAPS".
I checked if this branch works with Isabelle 2024-RC2 with the hope that it will resolve the remaining problems. Initially it failed to build the TLA+ theories with: ``` Session...