[c0nstantine]

Thanks 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

[DonaldPShimoda]

Just a small FYI, but the language's name (for now) is Coq, not COQ.