| Safe Haskell | None |
|---|---|
| Language | GHC2021 |
Conformance.Lean.Retirement
Description
The retirement effect computed by the model after a real registration.
Synopsis
- data UpdateTerminal
- modelComparison :: LeanCheck (LiveI reg wal step obs cmp) UpdateTerminal step
- updateTerminalRow :: Theorem UpdateTerminal
Documentation
data UpdateTerminal Source #
The accepted retirement declaration.
modelComparison :: LeanCheck (LiveI reg wal step obs cmp) UpdateTerminal step Source #
Check burn, witness consumption, remaining holdings and the committed leaf.
updateTerminalRow :: Theorem UpdateTerminal Source #
The revision and statement digest resolved before the live clause runs.