Compilation of Regex to Lean

[algebraic-dev]

I think that we can generate lean code from the compiled regex in order to get some performance in the future :)

[pandaman64]

Integrating with re2c seems a promising approach for code generation. It supports multiple languages as targets but they are all C-like (Go, Rust), so there might be some difficulties for functional languages like Lean.

It would be very interesting if we can make it a certifying regex compiler, but it sounds like a research project😉