Syntax for elaboration time control flow.

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.