opaque Lake.DSL.dummyDir : System.FilePath

A dummy default constant for __dir__ to make it type check outside Lakefile elaboration (e.g., when editing).

opaque Lake.DSL.dummyGetConfig? : Lean.Name → Option String

A dummy default constant for get_config to make it type check outside Lakefile elaboration (e.g., when editing).

def Lake.DSL.dirConst : Lean.ParserDescr

A macro that expands to the path of package's directory during the Lakefile's elaboration.

Equations

• Lake.DSL.dirConst = Lean.ParserDescr.node `Lake.DSL.dirConst 1024 (Lean.ParserDescr.symbol "__dir__")

def Lake.DSL.elabDirConst : Lean.Elab.Term.TermElab

Equations

• One or more equations did not get rendered due to their size.

def Lake.DSL.getConfig : Lean.ParserDescr

A macro that expands to the specified configuration option (or none, if the option has not been set) during the Lakefile's elaboration.

Configuration arguments are set either via the Lake CLI (by the -K option) or via the with clause in a require statement.

Equations

• Lake.DSL.getConfig = Lean.ParserDescr.node `Lake.DSL.getConfig 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "get_config? ") (Lean.ParserDescr.const `ident))

def Lake.DSL.elabGetConfig : Lean.Elab.Term.TermElab

Equations

• One or more equations did not get rendered due to their size.