diff --git a/library/algebra/function.lean b/library/algebra/function.lean index 4bb598290..8649d5100 100644 --- a/library/algebra/function.lean +++ b/library/algebra/function.lean @@ -45,7 +45,5 @@ infixr ∘' := dcompose infixl on := on_fun infixr $ := app notation f `-[` op `]-` g := combine f op g --- Trick for using any binary function as infix operator -notation a `⟨` f `⟩` b := f a b end function