Direction (Left / Right)

A two-element enumeration shared across phonology and computability substrates that need a notion of left-vs-right (FST scan direction, context side, harmony spread direction, etc.). Promoted to Core/ so that Theories/Phonology/Process/Alternation.lean::Side and Core/Computability/Subregular/Function/Subsequential.lean::Direction do not duplicate the same inductive type with the same case names.

Consumers should open Core (or qualify) and use Direction.left / Direction.right directly. Phonology-side aliases Side := Direction are acceptable when the Side name reads more naturally for the local context (e.g., "context side" of a tier rule), but the underlying type must be this one.

inductive Core.Direction : Type

A left-vs-right enumeration.

• left : Direction
• right : Direction

@[implicit_reducible]

instance Core.instDecidableEqDirection : DecidableEq Direction

Equations

• Core.instDecidableEqDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.instReprDirection.repr : Direction → Nat → Std.Format

Equations

• Core.instReprDirection.repr Core.Direction.left prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Direction.left")).group prec✝
• Core.instReprDirection.repr Core.Direction.right prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Direction.right")).group prec✝

@[implicit_reducible]

instance Core.instReprDirection : Repr Direction

Equations

• Core.instReprDirection = { reprPrec := Core.instReprDirection.repr }

def Core.Direction.flip : Direction → Direction

Flip a direction: left ↔ right.

Equations

• Core.Direction.left.flip = Core.Direction.right
• Core.Direction.right.flip = Core.Direction.left

@[simp]

theorem Core.Direction.flip_flip (d : Direction) : d.flip.flip = d

@[simp]

theorem Core.Direction.flip_left : left.flip = right

@[simp]

theorem Core.Direction.flip_right : right.flip = left