<p>You need to add a space after the <code>d</code>, before the <code>]</code>.</p>

CC BY-SA 4.0
2023-06-01T19:30:19.847Z
2023-06-01T19:30:19.847Z
Pierre Jouvelot
<p>The following problem arises when I try to define a new notation. I have a function</p>
<pre><code>f : A -&gt; A -&gt; A -&gt; A -&gt; Type
</code></pre>
<p>Then I want special notation for the value of this function.</p>
<pre><code>Notation &quot; [ a b c d] &quot; := (f a b c d).
</code></pre>
<p>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?</p>

CC BY-SA 4.0
2023-06-01T18:39:53.273Z
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.
paulotorrens
CC BY-SA 4.0
2023-06-01T18:47:39.500Z
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.
coqbeginner
CC BY-SA 4.0
2023-06-01T20:06:55.653Z
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 `]`.
paulotorrens
CC BY-SA 4.0
2023-06-05T13:21:39.693Z
As cstheory is for research-level questions, this questions might be more suitable for http://proofassistants.stackexchange.com.
gadmm
<dependent-type><interactive-proofs><coq>
Notation problem
coqbeginner
# Notation problem

(Asked by: username_0 on 2023-06-01)

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?

**Tags:** dependent-type, interactive-proofs, coq

> **Comments:**
> **username_1**: 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.  
> **username_0**: 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.  
> **username_1**: 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 `]`.  
> **username_2**: As cstheory is for research-level questions, this questions might be more suitable for http://proofassistants.stackexchange.com.  

---

## 1 answers

### Answer by username_3 on 2023-06-01. Score: 3

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


---

