pith. machine review for the scientific record. sign in
def definition def or abbrev

tickToBits

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

formal statement (Lean)

  53def tickToBits (t : TickIndex) : Fin 2 × Fin 2 × Fin 2 :=

proof body

Definition body.

  54  (⟨t.val % 2, Nat.mod_lt _ (by norm_num)⟩,
  55   ⟨(t.val / 2) % 2, Nat.mod_lt _ (by norm_num)⟩,
  56   ⟨(t.val / 4) % 2, Nat.mod_lt _ (by norm_num)⟩)
  57
  58/-- Reconstruct tick index from 3 bits. -/

used by (1)

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

depends on (4)

Lean names referenced from this declaration's body.