Script Declarations

DSL definitions to define a Lake script for a package.

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.

Example

/-- Display a greeting -/
script «script-name» (args) do
  if h : 0 < args.length then
    IO.println s!"Hello, {args[0]'h}!"
  else
    IO.println "Hello, world!"
  return 0

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.