source
def Lake.configField :
Lean.ParserDescr
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lake.configDecl :
Lean.ParserDescr

An tailored `structure` command for producing Lake configuration data types. It supports additional field annotations and generates additional metadata used during serialization to/from Lean and TOML.

It is not a perfect superset of `structure`, but instead just the parts that are / could be reasonably needed by Lake.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lake.expandConfigDecl :
Lean.Macro
Equations

- One or more equations did not get rendered due to their size.

Instances For