def Lake.DSL.fromPath : Lean.ParserDescr

Equations

• Lake.DSL.fromPath = Lean.ParserDescr.nodeWithAntiquot "fromPath" `Lake.DSL.fromPath (Lean.ParserDescr.cat `term 0)

def Lake.DSL.fromGit : Lean.ParserDescr

Equations

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

def Lake.DSL.depSpec : Lean.ParserDescr

Equations

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

def Lake.DSL.expandDepSpec : Lean.TSyntax `Lake.DSL.depSpec → Lean.MacroM Lean.Command

Equations

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

def Lake.DSL.requireDecl : Lean.ParserDescr

Adds a new package dependency to the workspace. Has two forms:

require foo from "path"/"to"/"local"/"package" with NameMap.empty
require bar from git "url.git"@"rev"/"optional"/"path-to"/"dir-with-pkg"

Either form supports the optional with clause. The @"rev" and /"path"/"dir" parts of the git form of require are optional.

The elements of both the from and with clauses are proper terms so normal computation is supported within them (though parentheses made be required to disambiguate the syntax).

Equations

• Lake.DSL.requireDecl = Lean.ParserDescr.node `Lake.DSL.requireDecl 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "require ") Lake.DSL.depSpec)