class Cslib.Automata.Acceptor (A : Type u) (Symbol : outParam (Type v)) : Type (max u v)

An Acceptor is a machine that recognises strings (lists of symbols in an alphabet).

• Accepts (a : A) (xs : List Symbol) : Prop

  Predicate that establishes whether a string xs is accepted.

def Cslib.Automata.Acceptor.language {Symbol : Type v} {A : Type u_1} [Acceptor A Symbol] (a : A) : Language Symbol

The language of an Acceptor is the set of strings it Accepts.

Equations

• Cslib.Automata.Acceptor.language a = {xs : List Symbol | Cslib.Automata.Acceptor.Accepts a xs}

@[simp]

theorem Cslib.Automata.Acceptor.mem_language {Symbol : Type v} {A : Type u_1} [Acceptor A Symbol] (a : A) (xs : List Symbol) : xs ∈ language a ↔ Accepts a xs

A string is in the language of an acceptor iff the acceptor accepts it.