Documentation

Lake.DSL.Meta

Syntax for elaboration time control flow.

source
@[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 α
source
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.
Instances For
    source
    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.
    Instances For
      source
      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.
      Instances For
        source
        @[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 α
        source
        def Lake.DSL.toExprIO {α : Type} [Lean.ToExpr α] (x : IO α) :
        IO Lean.Expr
        Equations
        Instances For
          source
          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
          Instances For
            source
            def Lake.DSL.elabRunIO :
            Lean.Elab.Term.TermElab
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              ToExpr Instances #

              source
              instance Lake.DSL.instToExprFilePath :
              Lean.ToExpr Lake.FilePath
              Equations