def Lean.Elab.ConfigEval.EvalTerm.withSimpleEvalStx {α : Type} (indTypeName : Name) (evalStxImpl : String → TSyntaxArray `term → TermElabM (α × Expr)) : Term → TermElabM (α × Expr)

Wrapper to handle atomic identifiers and dotted identifiers.

def Lean.Elab.ConfigEval.EvalTerm.checkExpectedNumberOfArguments (ctor : Name) (expected : Nat) (args : TSyntaxArray `term) : TermElabM Unit

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

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