Langlib

Langlib.Classes.DeterministicContextFree.Examples.AbcStack

Shared stack alphabet for the `a b c` DPDA examples #

ABCStack is the pushdown stack alphabet shared by the deterministic pushdown automata recognising {aⁿbⁿcᵐ} (Langlib.Classes.DeterministicContextFree.Examples.AnBnCm) and {aⁿbᵐcᵐ} (Langlib.Classes.DeterministicContextFree.Examples.AnBmCm). It lives in its own leaf module so that neither example needs to publicly depend on the other.

inductive DCFLIntersection.ABCStack :

bottom : ABCStack
mark : ABCStack

Instances For

@[instance_reducible]

instance DCFLIntersection.instDecidableEqABCStack :

DecidableEq ABCStack

Equations

DCFLIntersection.instDecidableEqABCStack x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DCFLIntersection.instFintypeABCStack :

Fintype ABCStack

Equations

DCFLIntersection.instFintypeABCStack = Fintype.ofList [DCFLIntersection.ABCStack.bottom , DCFLIntersection.ABCStack.mark ] DCFLIntersection.instFintypeABCStack._proof_1