Lean4
/-- Checks that the input `Expr` represents a proof produced by `(e)rw` and returns the types of the
LHS of the equality being written (one from the target, the other from the lemma used).
These will be defeq, but not necessarily reducibly so.
-/
def extractRewriteEq (e : Expr) : MetaM (Expr × Expr) := do
let (``Eq.mpr, #[_, _, e, _]) := e.getAppFnArgs |
throwError"Unexpected term produced by `erw`, head is not an `Eq.mpr`."
let (``id, #[ty, e]) := e.getAppFnArgs |
throwError"Unexpected term produced by `erw`, not of the form: `Eq.mpr (id _) _`."
let some (_, tgt, _) := ty.eq? |
throwError"Unexpected term produced by `erw`, type hint is not an equality."
let some (_, inferred, _) := (← inferType e).eq? |
throwError"Unexpected term produced by `erw`, inferred type is not an equality."
return (tgt, inferred)
