Ioannis Filippidis

No, #34 did not address tuple declarations in set constructors and constant quantifiers. I now reused some of the functionality from #34 to implement: - tuple declarations in set constructors...

This implementation of tuple declarations is currently at: https://github.com/johnyf/tlapm/tree/tuple_declarations

When commits that are included in the branch are merged into branch `main`, the list of commits between branch `main` and the branch of the pull request (here branch `tuply_concrete_syntax_tree`)...

Thank you for reporting this error. Before the function https://github.com/tlaplus/tlapm/blob/b82e2fd049c5bc1b14508ae16890666c6928975f/src/backend/smt.ml#L492 is called, all De Bruijn indices are positive. Within the function `process_obligation`, an expression `Ix -1` arises, and raises an...

Thank you for reviewing the changes and building the website, I have updated the changes to correct the errors. In the renaming of filepaths to lowercase, there were links in...

Rebased the changes onto branch `main`. The changes are: - release tag name of the form `YEAR_MM_DD_UTC_HH_MM` - running `release.yml` when it changes, and twice a year - showing contents...

Yes, the original fix for quoting environment variables was to code that is not in the current `main` branch. The automated building with `cron` could be omitted. Added the DCO...

This error means that `tlapm` needs to expand the operator `A`, but cannot expand `A`, because `A` is a declared operator. So `tlapm` cannot proceed with trying to prove this...

Thank you for reporting this issue. Based on discussions on the website Stack Overflow about the error code `-1073741515` in Windows, when this signed decimal integer value is interpreted as...

Thank you @ahelwer for suggesting documenting this information in the installer's messages. Thank you @lemmy for noting that TLAPS is known to reliably work on WSL/WSL2, suggesting transitioning to WSL2,...