def Lake.configField : Lean.ParserDescr

Equations

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

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.

def Lake.expandConfigDecl : Lean.Macro

Equations

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