<div dir="ltr"><div>I meant syntax declaration, not a pattern synonym.<br><br></div>Jesper<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Oct 7, 2015 at 2:34 PM, Jesper Cockx <span dir="ltr">&lt;<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>I&#39;m not sure if I understand. With _∋_, you could write<span><br></span><br></div><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">foo123foo = Foo ∋ foo&#39;<br>
<br>foo = Foo ∋ foo&#39; (T ∋ f x) y<br></blockquote><div><br></div><div>You could also use a pattern synonym to put the type signature after the term instead of before:<br><br><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">El : ∀ {a} (A : Set a) → A → A<br>El A x = x<br><br>syntax El A x = x ∈ A<br></blockquote><div> </div><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote"><div>foo123foo = foo&#39; ∈ Foo<span class=""><br>
<br>foo = foo&#39; (f x ∈ T) y ∈ Foo</span></div></blockquote><div> </div> <br></div><blockquote><br></blockquote></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Oct 7, 2015 at 2:01 PM, Sergei Meshveliani <span dir="ltr">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span>On Wed, 2015-10-07 at 13:54 +0200, Jesper Cockx wrote:<br>
&gt; From Function.agda in the standard library:<br>
&gt;<br>
&gt;         -- In Agda you cannot annotate every subexpression with a type<br>
&gt;         -- signature. This function can be used instead.<br>
&gt;<br>
&gt;         _∋_ : ∀ {a} (A : Set a) → A → A<br>
&gt;         A ∋ x = x<br>
&gt;<br>
&gt;<br>
&gt; Does this solve your problem?<br>
&gt;<br>
<br>
</span>No. I meant the implementation part -- the part after  `` = &#39;&#39;.<br>
<br>
------<br>
Sergei<br>
<div><div><br>
<br>
<br>
<br>
&gt; On Wed, Oct 7, 2015 at 1:41 PM, Sergei Meshveliani &lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;<br>
&gt; wrote:<br>
&gt;         Is it possible to allow in Language the syntax like<br>
&gt;<br>
&gt;           foo123foo = foo&#39; : Foo<br>
&gt;<br>
&gt;         (instead of<br>
&gt;           foo123foo : Foo<br>
&gt;           foo123foo = foo&#39;<br>
&gt;         )<br>
&gt;         ?<br>
&gt;<br>
&gt;         And one also could think of expressions like<br>
&gt;<br>
&gt;           foo = foo&#39; (f x : T) y  : Foo<br>
&gt;<br>
&gt;         This will make programs a bit more readable.<br>
&gt;<br>
&gt;         Regards,<br>
&gt;<br>
&gt;         ------<br>
&gt;         Sergei<br>
&gt;<br>
&gt;         _______________________________________________<br>
&gt;         Agda mailing list<br>
&gt;         <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
&gt;         <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt;<br>
&gt;<br>
<br>
<br>
</div></div></blockquote></div><br></div>
</div></div></blockquote></div><br></div>