TLX.Functions (TLX v0.5.2)

Function constructor, function set, and Cartesian product for TLA+ expressions.

These are essential for realistic TypeOK invariants: flags \in [Nodes -> BOOLEAN], initial functions like vote_counts = [n \in Nodes |-> 0], and product types like messages \subseteq (Nodes \X Nodes).

fn_of(:x, :set, expr)     # [x \in set |-> expr]
fn_set(domain, range)     # [domain -> range]
cross(a, b)               # (a \X b)

Summary

Functions

cross(a, b)

Cartesian product: (a \X b)

fn_of(var, set, expr)

Function constructor: [var \in set |-> expr]

fn_set(domain, range)

Function set (type of all functions from domain to range): [domain -> range]