module module

`IndisputableMonolith.Foundation.Atomicity`

show as: view Lean formalization →

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

generate prose now

declarations in this module (26)

abbrev Precedence L33
def isMinimalIn L40
lemma exists_minimal_in L50
def topoSort L72
lemma topoSort_perm L91
lemma topoSort_respects L139
structure Schedule L202
def postAtTick L211
theorem exists_sequential_schedule L217
theorem sequential_preserves_conservation L234
theorem atomic_tick L258
def enum L282
lemma enum_surjective L285
def eligible L289
lemma eligible_mono L292
lemma exists_minimal_eligible L299
structure Candidate L315
lemma exists_candidate_index L322
def chooseCandidate L332
lemma chooseCandidate_none_iff L348
lemma chooseCandidate_some_spec L357
def minIndex L369
lemma minIndex_spec L372
lemma minIndex_min L377
def scheduleByMinIndex L385
theorem atomic_tick_countable L429