IndisputableMonolith.Masses.Ribbons.Tick

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Masses
   5namespace Ribbons
   6
   7/-! model -- auxiliary tick helpers for ribbon demos.
   8The predicates below support the narrative ribbon construction; they are not
   9used in any proven theorems yet. Categorised as `Model`./-
  10
  11/-- Eight‑tick clock. -/
  12abbrev Tick := Fin 8
  13
  14end Ribbons
  15end Masses
  16end IndisputableMonolith
  17