Documentation

Lake.DSL.Script

Script Declarations #

DSL definitions to define a Lake script for a package.

source
def Lake.DSL.scriptDeclSpec :
Lean.ParserDescr
Instances For
    source
    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
    Instances For
      source
      def Lake.DSL.expandScriptDecl :
      Lean.Macro
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For