3 ms·
And here the formalized proof in less than 150 lines of code (in Agda) for Brzozowski Derivatives for regex matching (and additional regular languages theorems)
by evolveyourmind 4y ago
And here the formalized proof in less than 150 lines of code (in Agda) for Brzozowski Derivatives for regex matching (and additional regular languages theorems): https://github.com/desi-ivanov/agda-regexp-automata https://github.com/desi-ivanov/agda-regexp-automata
- c0nstantine 4y agoThanks for sharing. I am not familiar with Agda. Will take a look. There is somewhat similar code in COQ: https://github.com/coq-community/regexp-Brzozowski https://github.com/coq-community/regexp-Brzozowski
- DonaldPShimoda 4y agoJust a small FYI, but the language's name (for now) is Coq, not COQ.