diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean index 9b9473157a..331e0e6b51 100644 --- a/src/Lean/Elab/BuiltinNotation.lean +++ b/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) := diff --git a/tests/lean/cdotAtSimpArg.lean b/tests/lean/cdotAtSimpArg.lean index e57cb130fd..70176d1b18 100644 --- a/tests/lean/cdotAtSimpArg.lean +++ b/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 [.^.] diff --git a/tests/lean/cdotAtSimpArg.lean.expected.out b/tests/lean/cdotAtSimpArg.lean.expected.out index 37cb79eba0..af8462a7c1 100644 --- a/tests/lean/cdotAtSimpArg.lean.expected.out +++ b/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