Lean4
/-- A list of all the congruence strategies used by `Lean.MVarId.congrCore!`.
-/
def congrPasses! : List (String × (Congr!.Config → MVarId → MetaM (Option (List MVarId)))) :=
[("user congr", userCongr?), ("hcongr lemma", smartHCongr?), ("congr simp lemma", when (·.useCongrSimp) congrSimp?),
("Subsingleton.helim", fun _ => subsingletonHelim?), ("BEq instances", when (·.beqEq) fun _ => beqInst?),
("obvious funext", fun _ => obviousFunext?), ("obvious hfunext", fun _ => obviousHfunext?),
("congr_implies", fun _ => congrImplies?'), ("congr_pi", fun _ => congrPi?)]
where/-- Conditionally runs a congruence strategy depending on the predicate `b` applied to the config.
-/
when (b : Congr!.Config → Bool) (f : Congr!.Config → MVarId → MetaM (Option (List MVarId))) (config : Congr!.Config)
(mvar : MVarId) : MetaM (Option (List MVarId)) := do
unless b config do
return none
f config mvar
