Commit 2023-02-18 15:40 3103b623

View on Github →

feat: port/Computability.NFA (#2338) Port NFA's from mathlib3

Estimated changes

Modified Mathlib.lean

Created Mathlib/Computability/NFA.lean

added def DFA.toNFA

added theorem DFA.toNFA_correct

added theorem DFA.toNFA_evalFrom_match

added def NFA.accepts

added def NFA.eval

added def NFA.evalFrom

added theorem NFA.evalFrom_append_singleton

added theorem NFA.evalFrom_nil

added theorem NFA.evalFrom_singleton

added theorem NFA.eval_append_singleton

added theorem NFA.eval_nil

added theorem NFA.eval_singleton

added theorem NFA.mem_accepts

added theorem NFA.mem_stepSet

added theorem NFA.pumping_lemma

added def NFA.stepSet

added theorem NFA.stepSet_empty

added def NFA.toDFA

added theorem NFA.toDFA_correct

added structure NFA