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
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lake.DSL.elabMetaIf :
    Lean.Elab.Command.CommandElab
    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 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
        • One or more equations did not get rendered due to their size.
        Instances For