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?

  • $\begingroup$ The right-hand side needs to be in parantheses. I.e., you want Notation "[ a b c d ]" := (f a b c d). in here. $\endgroup$ Commented Jun 1, 2023 at 18:39
  • 1
    $\begingroup$ I edited to what I had from the beginning in my code, exactly what you wrote and it gives the problem. Sorry for the confusion. $\endgroup$ Commented Jun 1, 2023 at 18:47
  • $\begingroup$ Oh, the issue is that it's seeing d] as a token. Notice that in my comment, I have added a space between d and ]. $\endgroup$ Commented Jun 1, 2023 at 20:06
  • $\begingroup$ As cstheory is for research-level questions, this questions might be more suitable for proofassistants.stackexchange.com. $\endgroup$
    – gadmm
    Commented Jun 5, 2023 at 13:21

1 Answer 1


You need to add a space after the d, before the ].


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.