Lean4
/-- Auxiliary function for `getRawProjections`.
Find custom projections, automatically found by simps.
These come from `DFunLike` and `SetLike` instances. -/
def findAutomaticProjections (str : Name) (projs : Array ParsedProjectionData) : CoreM (Array ParsedProjectionData) :=
do
let strDecl ← getConstInfo str
trace[simps.debug]"debug: {projs}"
MetaM.run' <|
TermElabM.run' (s := { levelNames := strDecl.levelParams }) <|
forallTelescope strDecl.type fun args _ ↦ do
let projs ←
projs.mapM fun proj => do
if let some (projExpr, projName) := ← findAutomaticProjectionsAux str proj args then
unless ← isDefEq projExpr proj.expr?.get! do
throwError "The projection {proj.newName } is not definitionally equal to an application \
of {projName}:{(indentExpr proj.expr?.get!)}\nvs{indentExpr projExpr}"
if proj.isCustom then
trace[simps.verbose]"Warning: Projection {proj.newName} is given manually by the user, \
but it can be generated automatically."
return proj
trace[simps.verbose]"Using {(indentExpr projExpr)}\nfor projection {proj.newName}."
return { proj with expr? := some projExpr }
return proj
return projs
