libtlafmt 0.4.1

A formatter library for TLA+ specs, core of tlafmt
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/FiniteSets.tla
---
------------------------------ MODULE FiniteSets -------------------------------
LOCAL INSTANCE Naturals
LOCAL INSTANCE Sequences
(*************************************************************************)
  (* Imports the definitions from Naturals and Sequences, but doesn't      *)
  (* export them.                                                          *)
  (*************************************************************************)

IsFiniteSet(S) ==
    (*************************************************************************)
  (* A set S is finite iff there is a finite sequence containing all its   *)
  (* elements.                                                             *)
  (*************************************************************************)
    \E seq \in Seq(S): \A s \in S: \E n \in 1..Len(seq): seq[n] = s

Cardinality(S) ==
    (*************************************************************************)
  (* Cardinality is defined only for finite sets.                          *)
  (*************************************************************************)
    LET CS[T \in SUBSET S] == IF T = {} THEN 0
    ELSE 1 + CS[T \ {CHOOSE x: x \in T}]
    IN CS[S]
================================================================================