All operators are more or less a verbatim translation following Translation.md
For recursive operators, we introduce a naive recursive translation (with prefix TLC_), and a fold-based translation for Apalache. The non-recursive versions are obviously more free-form and probably deserve additional scrutiny.
Add the definitions from
helpers.pyin TLA+.All operators are more or less a verbatim translation following
Translation.mdFor recursive operators, we introduce a naive recursive translation (with prefix
TLC_), and a fold-based translation for Apalache. The non-recursive versions are obviously more free-form and probably deserve additional scrutiny.@Kukovec @konnov for review