def Lean.Elab.ConfigEval.EvalExpr.withSimpleEvalExpr {α : Type} (c : Name) (evalExprImpl : String → Array Expr → MetaM α) : Expr → MetaM α

Equations

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

def Lean.Elab.ConfigEval.ensureEvalExpr (vis? : Option (TSyntax `Lean.Parser.Command.visibility)) (kind : TSyntax `Lean.Parser.Term.attrKind) (cmdRef typeRef : Syntax) (type : Expr) : Command.CommandElabM Unit

Ensures an EvalExpr instance exists for the given type by deriving one if necessary. Derivation can handle EvalExpr instance for nonrecursive inductive types without universes, parameters, or indices, and which only does simple recursion.

unsafe def Lean.Elab.ConfigEval.evalMetaEval (α : Type) (typeName : Name) (moduleName? : Option Name) (e : Expr) : MetaM α

def Lean.Elab.ConfigEval.deriveEvalExprUsingMetaEval (vis? : Option (TSyntax `Lean.Parser.Command.visibility)) (kind : TSyntax `Lean.Parser.Term.attrKind) (cmdRef typeRef : Syntax) (type : Expr) : Command.CommandElabM Unit

Creates an EvalExpr instance that uses Meta.evalExpr to compile and evaluate the expression.