abbrev definition def or abbrev

`AtomicTick`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  58abbrev AtomicTick := Recognition.AtomicTick

Definition body.

  59
  60/-- Re-export: Atomicity theorem (T2). -/

From the project-wide theorem graph. These declarations reference this one in their body.

AtomicTick in IndisputableMonolith.Chain decl_use
T2_atomicity in IndisputableMonolith.Chain decl_use
accountAt in IndisputableMonolith.LedgerPostingAdjacency decl_use
AccountRS in IndisputableMonolith.LedgerPostingAdjacency decl_use
accountRS_atomicTick in IndisputableMonolith.LedgerPostingAdjacency decl_use
legalAtomicTick_oneBitDiff in IndisputableMonolith.LedgerPostingAdjacency decl_use
postedAt_accountAt in IndisputableMonolith.LedgerPostingAdjacency decl_use
stepAt in IndisputableMonolith.LedgerPostingAdjacency decl_use
stepAt_isPostingStep in IndisputableMonolith.LedgerPostingAdjacency decl_use
stepAt_oneBitDiff in IndisputableMonolith.LedgerPostingAdjacency decl_use
AtomicTick in IndisputableMonolith.Recognition decl_use
T2_atomicity in IndisputableMonolith.Recognition decl_use
postedAt in IndisputableMonolith.Recognition.Cycle3 decl_use
SimpleTicks in IndisputableMonolith.Recognition.ModelingExamples decl_use
T2_atomicity in IndisputableMonolith.RRF.Core.Recognition decl_use

Lean names referenced from this declaration's body.