Documentation

Lake.Config.Script

@[reducible, inline]
abbrev Lake.ScriptM (α : Type) :

The type of a Script's monad.

It is an IO monad equipped information about the Lake configuration.

Equations
    Instances For
      @[reducible, inline]

      The type of a Script's function.

      It is similar to the main function's signature, except the monad is also equipped with information about the Lake configuration.

      Equations
        Instances For
          structure Lake.Script :

          A package Script is a named ScriptFn definition with a some optional documentation.

          It can be run by lake run <name> [-- <args>].

          Instances For

            Run the script with the specified CLI args.

            Equations
              Instances For