def Lake.DSL.scriptDeclSpec : Lean.ParserDescr

Equations

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

def Lake.DSL.scriptDecl : Lean.ParserDescr

Define a new Lake script for the package. Has two forms:

script «script-name» (args) do /- ... -/
script «script-name» (args) := ...

Equations

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

def Lake.DSL.expandScriptDecl : Lean.Macro

Equations

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