English
The data part of a continuation is a list of lists that records the data on the stack, constructed via contStack.
Русский
Часть данных продолжения представляет собой список списков, хранящий данные на стеке, строимый функцией contStack.
LaTeX
$$$\\operatorname{contStack}(\\text{Cont.halt}) = []$, and for other constructors, $\\operatorname{contStack}(\\text{Cont.cons}_1(fs,ns,k)) = ns :: \\operatorname{contStack}(k)$, etc.$$
Lean4
/-- The data part of a continuation is a list of lists, which is encoded on the `stack` stack
using `trLList`. -/
@[simp]
def contStack : Cont → List (List ℕ)
| Cont.halt => []
| Cont.cons₁ _ ns k => ns :: contStack k
| Cont.cons₂ ns k => ns :: contStack k
| Cont.comp _ k => contStack k
| Cont.fix _ k => contStack k
