def
definition
def or abbrev
SimpleTicks
show as:
view Lean formalization →
formal statement (Lean)
32def SimpleTicks : Nat → Bool → Prop := fun t v => v = (t % 2 == 1)
proof body
Definition body.
33
34instance : AtomicTick SimpleStructure := {
35 postedAt := SimpleTicks,
36 unique_post := by
37 intro t
38 use (t % 2 == 1)
39 constructor
40 · rfl
41 · intro u hu
42 simp [SimpleTicks] at hu
43 exact hu
44}
45
46/-- Example of BoundedStep on Bool with degree 1. -/
47instance : BoundedStep Bool 1 := {
48 step := SimpleStructure.R,
49 neighbors := fun b => if b then {false} else {true},
50 step_iff_mem := by
51 intro a b
52 simp [SimpleStructure]
53 cases a <;> cases b <;> simp
54}
55
56end ModelingExamples
57end IndisputableMonolith