katydid / regex-derivatives-coq

Apache License 2.0
21 stars 7 forks source link

split regular expression into itself and empty str #156

Closed awalterschulze closed 3 years ago

awalterschulze commented 3 years ago

Review, but DO NOT MERGE This relies on the #153 merging first, so I will make sure it merges in the right order.

This is the start of Brzozowski's proof of denotation.

awalterschulze commented 3 years ago

Discussed offline: merging now and will post review