Commit 2023-02-16 08:49 1c14085a

View on Github →

feat: port Computability.DFA (#2317)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Computability/DFA.lean

added def DFA.accepts

added def DFA.eval

added def DFA.evalFrom

added theorem DFA.evalFrom_append_singleton

added theorem DFA.evalFrom_nil

added theorem DFA.evalFrom_of_append

added theorem DFA.evalFrom_of_pow

added theorem DFA.evalFrom_singleton

added theorem DFA.evalFrom_split

added theorem DFA.eval_append_singleton

added theorem DFA.eval_nil

added theorem DFA.eval_singleton

added theorem DFA.mem_accepts

added theorem DFA.pumping_lemma

added structure DFA