knowsys / Formale-Systeme-in-LEAN

LEAN4 formalization of the undergraduate lecture "Formale Systeme" at TU Dresden (WIP)
Apache License 2.0
8 stars 0 forks source link

Grammar to NFA #4

Closed matzemathics closed 1 year ago

matzemathics commented 1 year ago

This completes the construction converting a Grammar to a NFA, together with proof converting derivations to runs and vice versa.