-1
$\begingroup$

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?

Improve this question
$\endgroup$
4
  • $\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$
    – paulotorrens
    Jun 1 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$
    – coqbeginner
    Jun 1 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$
    – paulotorrens
    Jun 1 at 20:06
  • $\begingroup$ As cstheory is for research-level questions, this questions might be more suitable for proofassistants.stackexchange.com. $\endgroup$
    – gadmm
    Jun 5 at 13:21

1 Answer 1

Reset to default
3
$\begingroup$

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

Improve this answer
$\endgroup$

Your Answer

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

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