# Construct Sets of Everything in TLA+ ## Metadata **Status**:: #x **Zettel**:: #zettel/literature **Created**:: [[2026-01-14]] **Parent**:: [[TLA+]] ## Power Set ``` SUBSET S ``` ## Sequence ``` S \X T \* repeat S 3 times [1..3 -> S] ``` Also see [SequencesExt](https://github.com/tlaplus/CommunityModules/blob/master/modules/SequencesExt.tla): ``` TupleOf(set, n) == [1..n -> set] \* TupleOf(set, 0) \union ... \union TupleOf(set, n) SeqOf(set, n) == UNION {[1..m -> set] : m \in 0..n} ``` ## Function ``` [S -> T] ``` ## Record ``` [f1: S1, ..., fn: Sn] ``` ## Manual ``` \* y1, ..., yn occur in e { e : y1 \in S1, ... , yn \in Sn } ```