Syntax for elaboration time control flow.

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

Equations

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