# TLA+ Fold Pattern ## Metadata **Status**:: #x **Zettel**:: #zettel/fleeting **Created**:: [[2026-01-12]] **Parent**:: [[TLA+]] **URL**:: [github.com](https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/CachingMemory/WriteThroughCache.tla) ## Synopsis Used by [[Lamport - Specifying Systems The TLA+ Language and Tools for Hardware and Software Engineers]] ```tla vmem == LET f[i \in 0 .. Len(memQ)] == IF i=0 THEN wmem ELSE IF memQ[i][2].op = "Rd" THEN f[i-1] ELSE [f[i-1] EXCEPT ![memQ[i][2].adr] = memQ[i][2].val] IN f[Len(memQ)] ``` Steps of the pattern: - Use `LET` to define a recursive function definitions `f` for steps `0..N`. - `f[i]` stores `acc` after step `i` - `f[0]` is the initial `acc`, and `f[N]` is the last result. - The definition `f[i \in 0..N]` is the i-th iteration of the folding. It can access the previous `acc` via `f[i - 1]`.