@[inline, reducible]

abbrev Lake.ScriptM (α : Type) : Type

The type of a Script's monad. IO equipped information about the Lake configuration.

Equations

• Lake.ScriptM = Lake.LakeT IO

@[inline, reducible]

abbrev Lake.ScriptFn : Type

The type of a Script's function. Similar to the main function's signature, except that its monad is also equipped with information about the Lake configuration.

Equations

• Lake.ScriptFn = (List String → Lake.ScriptM Lake.ExitCode)

structure Lake.Script : Type

• name : String

  The full name of the Script (e.g., pkg/script).

• fn : Lake.ScriptFn
• doc? : Option String

A package Script is a ScriptFn definition that is indexed by a String key and can be be run by lake run [-- ].

instance Lake.instInhabitedScript : Inhabited Lake.Script

Equations

• Lake.instInhabitedScript = { default := { name := default, fn := default, doc? := default } }

def Lake.Script.run (args : List String) (self : Lake.Script) : Lake.ScriptM Lake.ExitCode

Equations

• Lake.Script.run args self = Lake.Script.fn self args