Syntax for elaboration time control flow.

@[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 α

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.elabMetaIf : Lean.Elab.Command.CommandElab

Equations

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

@[implemented_by Lean.Meta.evalExpr]

opaque Lake.DSL.evalExpr (α : Type) (expectedType value : Lean.Expr) (safety : Lean.DefinitionSafety := Lean.DefinitionSafety.safe) : Lean.MetaM α

def Lake.DSL.toExprIO {α : Type} [Lean.ToExpr α] (x : IO α) : IO Lean.Expr

Equations

• Lake.DSL.toExprIO x = Lean.toExpr <$> x

def Lake.DSL.elabRunIO : Lean.Elab.Term.TermElab

Equations

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