title: How to define my own (recursive) Coq notations?
body: <p>I've started working a lot with <code>Ensemble</code>s now, because they are more flexible. To help me with that, I'm trying to define some convenient notations. The following is relatively easy, for example:</p>
  
  <pre><code>Notation "a ∈ S" := (@In _ S a)  (at level 80).
  </code></pre>
  
  <p>And I can add a similar bunch for the other binary set operators.</p>
  
  <p>But I'm having a lot of trouble with notations like this:</p>
  
  <pre><code>Notation "∀ x ∈ S , P" := (forall x, (x ∈ S) -&gt; P)  (at level 90).
  </code></pre>
  
  <p>It is accepted, but whenever I try to use it I get this error:</p>
  
  <blockquote>
    <p>Syntax error: "∈" expected after [constr:operconstr level 200] (in [constr:operconstr]).</p>
  </blockquote>
  
  <p><strong>Question 1:</strong> What am I doing wrong?</p>
  
  <p>For bonus points, can you tell me how to define a recursive notation for it? I've tried, but it seems to give me a whole new set of problems. Here's my attempt, a straightforward edit of the library definition:</p>
  
  <pre><code>Notation "∀ x .. y ∈ S , P" :=
    (forall x, (x ∈ S) -&gt; .. (forall y, (y ∈ S) -&gt; P) ..)
    (at level 200, x binder, y binder, right associativity).
  </code></pre>
  
  <p>I don't see why the library version in <code>Coq.Unicode.Utf8_core</code> should parse and mine shouldn't, but:</p>
  
  <blockquote>
    <p>Error: Cannot find where the recursive pattern starts.</p>
  </blockquote>
  
  <p><strong>Question 2:</strong> See question 1.</p>