Documentation

Lake.DSL.Script

source
def Lake.DSL.scriptDeclSpec :
Lean.ParserDescr
Instances For
    source
    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) := ...
    Instances For
      source
      def Lake.DSL.expandScriptDecl :
      Lean.Macro
      Instances For