Lean4
/-- Reassociates the morphisms in `type?` using the registered handlers,
using `reassocExprHom` as the default.
If `type?` is not given, it is assumed to be the type of `pf`.
Returns the proof of the lemma along with instance metavariables that need synthesis.
-/
def reassocExpr (pf : Expr) (type? : Option Expr) : MetaM (Expr × Array MVarId) := do
let pf ←
if let some type := type? then
mkExpectedTypeHint pf type
else
pure pf
forallTelescopeReducing (← inferType pf) fun xs _ => do
let pf := mkAppN pf xs
let handlers ← reassocImplRef.get
let (pf, insts) ←
handlers.firstM (fun h => h pf) <|> do
throwError"`reassoc` can only be used on terms about equality of (iso)morphisms"
return (← mkLambdaFVars xs pf, insts)
