202604221529

Theorems for sum of constant function

Add SumFunctionOnSetConst and SumFunctionConst stating that summing a
constant function over a finite set equals the constant times the
cardinality of the set, together with corresponding proofs and an
example in the doc comments.

[Feature]

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

202604061452

add ToBag operator (#123)

* add ToBag operator

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

* improve comment for ToBag operator

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

---------

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

202603110432

Update GitHub Actions workflows to use the new output syntax for sett…

202602261933

make syntax compatible with TLAPM (#120)

* make syntax compatible with TLAPM

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

* reformulation of comment on syntax not supported by TLAPS

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

---------

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

202601200755

two more theorems about folds (#119)

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

202601131539

Update SVGSerialize to use three-digit zero-padding for frame numbers…

202601110807

more theorems about folds (#118)

* more theorems about folds

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

* more theorems on folds

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

* theorems for SumFunction

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

* align statement of ReverseSubSeq

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

---------

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

202512162320

Remove tabs from VectorClocks.tla (#117)

TLAPM does not like tabs

Signed-off-by: Andrew Helwer <ahelwer@pm.me>

202512151634

Merge pull request #116 from tlaplus/fold_proofs

theorem library for fold operators

202511171707

Do not require CSV read/write operations to be state level.

Constant level is sufficient and allows TLC to cache the results.

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>