Lean4
/-- Find the argument of `nm` that appears in the first multiplicative (type-class) argument.
Returns 1 if there are no types with a multiplicative class as arguments.
E.g. `Prod.instGroup` returns 1, and `Pi.instOne` returns 2.
Note: we only consider the relevant argument (`(relevant_arg := ...)`) of each type-class.
E.g. `[Pow A N]` is a multiplicative type-class on `A`, not on `N`.
-/
def findMultiplicativeArg (nm : Name) : MetaM Nat := do
forallTelescopeReducing (← getConstInfo nm).type fun xs ty ↦ do
let env ← getEnv
let multArg? (tgt : Expr) : Option Nat := do
let c ← tgt.getAppFn.constName?
guard (findTranslation? env c).isSome
let relevantArg := (relevantArgAttr.find? env c).getD 0
let arg ← tgt.getArg? relevantArg
xs.findIdx?
(arg.containsFVar ·.fvarId!)
-- run the above check on all hypotheses and on the conclusion
let arg ←
OptionT.run <|
xs.firstM fun x ↦
OptionT.mk do
forallTelescope (← inferType x) fun _ys tgt ↦ return multArg? tgt
let arg := arg <|> multArg? ty
trace[to_additive_detail]"findMultiplicativeArg: {arg}"
return arg.getD 0
