The following problem arises when I try to define a new notation. I have a function
f : A -> A -> A -> A -> Type
Then I want special notation for the value of this function.
Notation " [ a b c d] " := (f a b c d).
The function needs 4 arguments by definition. However, Coq does not accepts this saying there are undefined references. Strangely, if I remove them (a and d specifically), so only b and c remain then it checks. I should maybe say that f is defined with an implicit argument. Even if I change it for an explicit argument the same thing occurs. Can someone explain what I am doing wrong?