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 : Lean.DefinitionSafety := Lean.DefinitionSafety.safe) :
Lean.Elab.TermElabM α
source
def Lake.DSL.expandCmdDo :
Lean.TSyntax `Lake.DSL.cmdDo → Array Lean.Command
Equations
    Instances For
      source
      def Lake.DSL.elabMetaIf :
      Lean.Elab.Command.CommandElab
      Equations
        Instances For
          source
          @[implemented_by Lean.Meta.evalExpr]
          opaque Lake.DSL.evalExpr (α : Type) (expectedType value : Lean.Expr) (safety : 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.elabRunIO :
              Lean.Elab.Term.TermElab
              Equations
                Instances For