pandaman64 / lean-regex

Apache License 2.0
19 stars 1 forks source link

Add the `sparse` node in the NFA, Intervals and Perl Classes #4

Closed algebraic-dev closed 5 months ago

algebraic-dev commented 6 months ago

I added

so now the library support things like \s and the inverse \S and [a-zA-Z0-9]

I'm not being able to think about a solution to one proof in the RegexCorrectness.

algebraic-dev commented 6 months ago

The continuous integration stuff is here too x.x I think that's a good idea to check the #5 first.

algebraic-dev commented 6 months ago

I'm trying to add some proofs about the well formedness of Intervals.

pandaman64 commented 6 months ago

Sorry, it's been a while since last I checked the repo and I didn't notice you have been doing great work! I have merged #5, but it would take a bit of time to check this PR. Thank you!

algebraic-dev commented 6 months ago

I need to organize a little bit because it's a messy code.

pandaman64 commented 5 months ago

Sorry for the late reply. I really appreciate your effort and contribution to the project.

I've reviewed the changes, and while there appears to be a small bug related to the handling of negations, I believe it's a minor issue that I can address separately. I'm going to go ahead and merge your pull request as-is and open a separate PR for a fix.

Thank you!