mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(computability): prove equivalence of NFAs and regular expressions

Open RussellEmerine opened this issue 3 years ago • 0 comments

Provide a way to convert NFAs to regular expressions and vice versa, and prove that the conversions accept the same language.

TODO: statement of some theorems, style, adding @[simp] annotations appropriately, conversions between DFAs and regular expressions

RussellEmerine avatar May 19 '22 21:05 RussellEmerine