Translate Maude modules to Lean specifications where terms, sort membership, equational, and rewriting relations are defined inductively. Hence, theorems about Maude specifications can be proven in Lean.
The syntax of the tool is
$ maude2lean <Maude source or JSON/YAML/TOML file>+ [-o <output file>]
where the arguments are either a Maude file or a JSON, YAML, or TOML specification to customize the translation. The available options are documented in this JSON schema, and most of them can also be passed as command-line options (use --help for a list). Examples are available in the test directory.
The installation requirements for maude2lean are Python 3.9 and the maude Python library. Wheels and bundles are available in the releases section of this repository.
For a detailed description of the translation, see Maude2Lean: Theorem proving for Maude specifications using Lean or its shorter conference version.