Lean4
/-- Try adding the lemma to the `RefinedDiscrTree`. -/
def addRewriteEntry (name : Name) (cinfo : ConstantInfo) : MetaM (List (RewriteLemma × List (Key × LazyEntry))) := do
-- we start with a fast-failing check to see if the lemma has the right shape
let .const head _ := cinfo.type.getForallBody.getAppFn |
return []
unless head == ``Eq || head == ``Iff do
return []
setMCtx
{ } -- recall that the metavariable context is not guaranteed to be empty at the start
let (_, _, eqn) ← forallMetaTelescope cinfo.type
let some (lhs, rhs) := eqOrIff? eqn |
return []
let badMatch e :=
e.getAppFn.isMVar ||
-- this extra check excludes general equality lemmas that apply at any equality
-- these are almost never useful, and there are very many of them.
e.eq?.any fun (α, l, r) => α.getAppFn.isMVar && l.getAppFn.isMVar && r.getAppFn.isMVar && l != r
if badMatch lhs then
if badMatch rhs then
return []
else
return [({ name, symm := true }, ← initializeLazyEntryWithEta rhs)]
else
let result := ({ name, symm := false }, ← initializeLazyEntryWithEta lhs)
if badMatch rhs || isMVarSwap lhs rhs then
return [result]
else
return [result, ({ name, symm := true }, ← initializeLazyEntryWithEta rhs)]
