Listed below is a brief description of each file of the formalization.
EffectiveBooleanAlgebra: main definition of effective boolean algebras.TTerm: main definitions and lemmas about transition terms.Definitions: contains the definitions of Extended Regular Expressions (ERE) and RLTL.Metrics: some simple metrics to show termination of theorems/definitions.ERE: the standard language-based match semantics and symbolic derivation rules for ERE.OmegaLanguage: contains the specification of omega languages.RLTL: contains the main theorem which connects derivative based unfolding with the formal semantics.
The project dependencies are listed in lakefile.lean.
The Lean version manager elan and the build tool lake will automatically download these dependency versions when you run lake build.
Lean has minimal platform requirements. The instructions provided above will work on Ubuntu 24.04 (x86-64) with git and curl installed. Other platforms, including Windows and macOS, are supported by Lean as well. Please see the Lean documentation for more details on platform support.