Script Declarations

DSL definitions to define a Lake script for a package.

def Lake.DSL.expandScriptDecl : Lean.Macro

Equations

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