def Lean.Elab.ConfigEval.makeStringMatcher (discr : Ident) (cases : Array (String × Term)) (onFail : Term) : TermElabM Term

Creates a decision tree to implement match discr with $cases* | _ => onFail, where discr : String.

Equations

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

def Lean.Elab.ConfigEval.withClassInstDeps (className : Name) (type : Expr) (extraDeps : Expr → TermElabM (Array Expr)) (mkCmd : Expr → TermElabM Command) : Command.CommandElabM Unit

Helper for deriving instances along with all dependencies. Given a one-parameter class className and a type type, uses pre-existing conditional instances to figure out which types would suffice to be implemented, then runs mkCmd on each type with fresh macro scopes.

The commands are generated and elaborated one at a time.

Equations

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