| Name | Type | Default value | Description |
|---|---|---|---|
| description | string | Free-text description of the settings | |
| source | string | Path to the input Maude file (or list of paths) | |
| module | string | Name of the Maude module to be transformed (or where to evaluate the metamodule) | |
| metamodule | string | Metarepresentation of the module to be transformed | |
| sort-renaming | object | Renaming for sort names | |
| kind-renaming | object | Renaming for kind names (any sort in the kind can be used as key) | |
| op-renaming | object | Renaming for operator names | |
| prefer-quotes | Boolean | False | Whether to eliminate symbols in operator names or prefer quotes to maintain them |
| use-notation | [string] | [] | Relations where infix notation is used instead of standard alphanumeric names |
| declare-notation | [string] | [] | Relations where infix notation is declared (even if not used, use-notation implies this) |
| with-ctor-predicate | Boolean | True | Whether to define a ctor_only predicate that holds only on constructor terms |
| with-error-free-opt | Boolean | False | Whether to optimize error-free kinds with a most general sort by removing sort membership premises for it |
| with-lemmas | Boolean | True | Whether to include simple lemmas derived from the base specification |
| with-aliases | Boolean | True | Whether to define aliases for the constructors of the inductive relations |
| with-repr | Boolean | True | Whether to define a pretty printing function for the terms |
| with-rules | Boolean | True | Whether to include rewrite rules and rewriting relations |
| with-frozen | Boolean | True | Whether the frozen attribute of operators is obeyed by skipping argument rewriting axioms |
| with-simp | Boolean | True | Whether to label statements with the simp, symm, trans, and congr attribute |
| with-axiom-simp | Boolean | False | Whether to include structural axioms in the simplifier (only useful if with-simp) |
| with-sort2kind | Boolean | True | Whether to define the 'kind' function from sorts to their corresponding kind types |
| with-derived-as-consts | Boolean | False | Whether operators that are not constructors are translated as constants outside the inductive datatype |
| with-derived-as-defs | Boolean | False | Whether compatible non-constructor operators are translated to Lean definitions outside the inductive datatype |
| with-native-bool | Boolean | False | Replace Maude's Bool sort by Lean's bool |
| split-eqe | [string] | [] | Split the application of an equation on top as a subrelation of eqe for the given kinds |
| has-sort-symbol | string | ⊳ | Infix notation for the sort membership relation |
| eqa-symbol | string | =A | Infix notation for equality module axioms |
| eqe-symbol | string | =E | Infix notation for equality modulo equations |
| rw-one-symbol | string | =>1 | Infix notation for the one-step rewriting relation |
| rw-star-symbol | string | =>* | Infix notation for the reflexive and transitive closure of the rewriting relation |
| outermost-namespace | string | Maude | Name of the outermost namespace (leave empty to omit that namespace) |
| with-original-stmt | Boolean | False | Include the original statement as a comment along with its translation |
| lean-version | integer | 3 | Lean version to generate code for |