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.

Equations

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

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

Equations

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

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.