Lean4
/-- Determine whether `e` will be handled as an atom by the `abel` tactic. The `match` in this
function should be preserved to be parallel in case-matching to that in the
`Mathlib.Tactic.Abel.eval` metaprogram. -/
def isAtom (e : Expr) : Bool :=
match e.getAppFnArgs with
| (``HAdd.hAdd, #[_, _, _, _, _, _]) | (``HSub.hSub, #[_, _, _, _, _, _]) | (``Neg.neg, #[_, _, _]) |
(``AddMonoid.nsmul, #[_, _, _, _]) | (``SubNegMonoid.zsmul, #[_, _, _, _]) |
(``SMul.smul, #[.const ``Int _, _, _, _, _]) | (``SMul.smul, #[.const ``Nat _, _, _, _, _]) |
(``HSMul.hSMul, #[.const ``Int _, _, _, _, _, _]) | (``HSMul.hSMul, #[.const ``Nat _, _, _, _, _, _]) |
(``smul, #[_, _, _, _]) | (``smulg, #[_, _, _, _]) => false
| _ => true
