fix: look through binop% variants in elabCDotFunctionAlias?

src/Lean/Elab/BuiltinNotation.lean

@@ -252,11 +252,21 @@ def elabCDotFunctionAlias? (stx : Term) : TermElabM (Option Expr) := do
       try Term.resolveId? f catch _ => return none
     else
       return none
-  | `(fun $binders* => binop% $f $a $b) =>
+  | `(fun $binders* => binop% $f $a $b)
+  | `(fun $binders* => binop_lazy% $f $a $b)
+  | `(fun $binders* => leftact% $f $a $b)
+  | `(fun $binders* => rightact% $f $a $b)
+  | `(fun $binders* => binrel% $f $a $b)
+  | `(fun $binders* => binrel_no_prop% $f $a $b) =>
     if binders == #[a, b] then
       try Term.resolveId? f catch _ => return none
     else
       return none
+  | `(fun $binders* => unop% $f $a) =>
+    if binders == #[a] then
+      try Term.resolveId? f catch _ => return none
+    else
+      return none
   | _ => return none
 where
   expandCDotArg? (stx : Term) : MacroM (Option Term) :=

tests/lean/cdotAtSimpArg.lean

@@ -1,6 +1,10 @@
+/-! Test `·` being able to refer to constants in `simp` -/
+
 example : ¬ true = false := by
   simp [(¬ ·)]
 
+/-! Test `binop%` -/
+
 example (h : y = 0) : x + y = x := by
   simp [(.+.)] -- Expands `HAdd.hAdd
   trace_state
@@ -14,3 +18,8 @@ example (h : y = 0) : x + y = x := by
   simp [Add.add]
   simp [h, Nat.add]
   done
+
+/-! Test `binop%` variant `rightact%` as well -/
+
+example (x y : Nat) : x ^ y = y ^ x := by
+  simp only [.^.]

tests/lean/cdotAtSimpArg.lean.expected.out

@@ -4,3 +4,6 @@ h : y = 0
 y x : Nat
 h : y = 0
 ⊢ Add.add x y = x
+cdotAtSimpArg.lean:24:39-25:17: error: unsolved goals
+x y : Nat
+⊢ Pow.pow x y = Pow.pow y x