IndisputableMonolith.Masses.Ribbons.Word

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Masses
   5namespace Ribbons
   6
   7structure Ribbon where
   8  start : Fin 8
   9  dir   : Bool
  10  bit   : Int
  11  tag   : Nat
  12
  13/-- A word is a list of ribbon syllables. -/
  14abbrev Word := List Ribbon
  15
  16end Ribbons
  17end Masses
  18end IndisputableMonolith
  19
  20
  21