Documentation

Lake.DSL.Meta

Syntax for elaboration time control flow.

@[implemented_by Lean.Elab.Term.evalTerm]

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
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      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
        @[implemented_by Lean.Meta.evalExpr]
        def Lake.DSL.toExprIO {α : Type} [Lean.ToExpr α] (x : IO α) :
        Equations
        Instances For

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

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

              ToExpr Instances #

              Equations