Scan direction

The orientation of a left-to-right vs right-to-left scan, shared by the transducer machines and the side-determinacy predicates of Core/Computability/Subregular/Function/. Extracted to its own leaf so the footprint-predicate file (SideDeterminacy.lean) does not have to depend on the transducer machine file just to name a left/right tag.

inductive Subregular.Direction : Type

The orientation of an FST scan: left consumes input head-first, right tail-first (via List.reverse conjugation). The two scan modes give rise to distinct function classes — isomorphic under reversal but not equal as subclasses of the regular functions over un-reversed strings.

• left : Direction
• right : Direction

@[implicit_reducible]

instance Subregular.instDecidableEqDirection : DecidableEq Direction

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Subregular.instReprDirection.repr Subregular.Direction.left prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Subregular.Direction.left")).group prec✝

@[implicit_reducible]

instance Subregular.instReprDirection : Repr Direction

Equations

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