congrCore! — Mathlib

Lean4
def congrCore! (config : Congr!.Config) (mvarId : MVarId) : MetaM (Option (List MVarId)) := do
  mvarId.checkNotAssigned `congr!
  let s ← saveState
  let mvarId ← mvarId.liftReflToEq
  for (passName, pass) in congrPasses! do
    try
      if let some mvarIds← pass config mvarId then
        trace[congr!]"pass succeeded: {passName}"
        return mvarIds
    catch e =>
      throwTacticEx `congr! mvarId m! "internal error in congruence pass {passName }, {e.toMessageData}"
    if ← mvarId.isAssigned then
      throwTacticEx `congr! mvarId s! "congruence pass {passName} assigned metavariable but failed"
  restoreState s
  trace[congr!]"no passes succeeded"
  return none
Похожие утверждения