def
definition
def or abbrev
postedAt
show as:
view Lean formalization →
formal statement (Lean)
25def postedAt : Nat → M.U → Prop := fun t v =>
proof body
Definition body.
26 v = ⟨t % 3, by
27 have : t % 3 < 3 := Nat.mod_lt _ (by decide : 0 < 3)
28 simpa using this⟩
29
30instance : AtomicTick M :=
31 { postedAt := postedAt
32 , unique_post := by
33 intro t
34 refine ⟨⟨t % 3, ?_⟩, ?_, ?_⟩
35 · have : t % 3 < 3 := Nat.mod_lt _ (by decide : 0 < 3)
36 simpa using this
37 · rfl
38 · intro u hu
39 simpa [postedAt] using hu }
40
41end Cycle3
42end IndisputableMonolith