Lean4
/-- Unfold a class projection if the instance is tagged with `@[default_instance]`.
This is used in the `unfold?` tactic in order to not show these unfolds to the user.
Similar to `Lean.Meta.unfoldProjInst?`. -/
def unfoldProjDefaultInst? (e : Expr) : MetaM (Option Expr) := do
let .const declName _ := e.getAppFn |
return none
let some { fromClass := true, ctorName, .. } ← getProjectionFnInfo? declName |
return none
let some (ConstantInfo.ctorInfo ci) := (← getEnv).find? ctorName |
return none
let defaults ← getDefaultInstances ci.induct
if defaults.isEmpty then
return none
let some e ← withDefault <| unfoldDefinition? e |
return none
let .proj _ i c := e.getAppFn |
return none
let .const inst _ := c.getAppFn |
return none
unless defaults.any (·.1 == inst) do
return none
let some r ← withReducibleAndInstances <| project? c i |
return none
return mkAppN r e.getAppArgs |>.headBeta
