Syntax for elaboration time control flow.

@[implemented_by Lean.Elab.Term.evalTerm]

opaque Lake.DSL.evalTerm (α : Type) (type : Lean.Expr) (value : Lean.Syntax) (safety : optParam Lean.DefinitionSafety Lean.DefinitionSafety.safe) : Lean.Elab.TermElabM α

def Lake.DSL.cmdDo : Lean.ParserDescr

The do command syntax groups multiple similarly indented commands together. The group can then be passed to another command that usually only accepts a single command (e.g., meta if).

Equations

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

def Lake.DSL.expandCmdDo : Lean.TSyntax `Lake.DSL.cmdDo → Array Lean.Command

Equations

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

def Lake.DSL.metaIf : Lean.ParserDescr

The meta if command has two forms:

meta if <c:term> then <a:command>
meta if <c:term> then <a:command> else <b:command>

It expands to the command a if the term c evaluates to true (at elaboration time). Otherwise, it expands to command b (if an else clause is provided).

One can use this command to specify, for example, external library targets only available on specific platforms:

meta if System.Platform.isWindows then
extern_lib winOnlyLib := ...
else meta if System.Platform.isOSX then
extern_lib macOnlyLib := ...
else
extern_lib linuxOnlyLib := ...

Equations

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

@[implemented_by Lean.Meta.evalExpr]

opaque Lake.DSL.evalExpr (α : Type) (expectedType : Lean.Expr) (value : Lean.Expr) (safety : optParam Lean.DefinitionSafety Lean.DefinitionSafety.safe) : Lean.MetaM α

def Lake.DSL.toExprIO {α : Type} [Lean.ToExpr α] (x : IO α) : IO Lean.Expr

Equations

• Lake.DSL.toExprIO x = Lean.toExpr <$> x

def Lake.DSL.runIO : Lean.ParserDescr

Executes a term of type IO α at elaboration-time and produces an expression corresponding to the result via ToExpr α.

Equations

• Lake.DSL.runIO = Lean.ParserDescr.node `Lake.DSL.runIO 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "run_io ") (Lean.ParserDescr.const `doSeq))

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

Equations

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