We just take over the Mathlib DFA/NFA automaton definition

def is_DFA {T : Type} (L : Language T) : Prop

A language is DFA-recognizable if it is accepted by some finite-state deterministic automaton in Mathlib's sense.

Equations

• is_DFA L = ∃ (σ : Type) (x : Fintype σ) (M : DFA T σ), M.accepts = L

def DFA.Class {T : Type} : Set (Language T)

The class of DFA-recognizable languages.

This lives under DFA.Class because the top-level name DFA is already used by Mathlib's automaton type.

Equations

• DFA.Class = setOf is_DFA