Removing notation for `Function.combine`

Stream: mathlib4

[Moritz Doll]

In !4#2869 the notation for the segment clashes with the notation for Function.combine. According to the VSCode search for -[ the notation for Function.combine is never used. Is there anyone opposed to removing it?

[Moritz Doll]

mnwe:

import Mathlib.Init.Function

def foo (a b c : Type _) : Type := sorry

notation "[" a "-[" c "]" b "]" => foo a b c

theorem foo_blubb : [a -[c] b] = foo a b c := sorry

[Eric Wieser]

In Lean 3 the notation was

notation f ` -[` op `]- ` g  := combine f op g

Is it the same in Lean 4 for docs4#Function.combine ?

[Moritz Doll]

yes, this is the notation that causes the above code to fail

[Moritz Doll]

it is defined in Mathlib.Init.Function