split regular expression into itself and empty str

awalterschulze / regex-reexamined-coq

Apache License 2.0

21 stars 7 forks source link

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