<div dir="ltr">From Function.agda in the standard library:<br><br><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">-- In Agda you cannot annotate every subexpression with a type<br>-- signature. This function can be used instead.<br><br>_∋_ : ∀ {a} (A : Set a) → A → A<br>A ∋ x = x<br></blockquote><div><br></div><div>Does this solve your problem?<br><br></div><div>Jesper <br></div><br></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Oct 7, 2015 at 1:41 PM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Is it possible to allow in Language the syntax like<br>
<br>
foo123foo = foo' : Foo<br>
<br>
(instead of<br>
foo123foo : Foo<br>
foo123foo = foo'<br>
)<br>
?<br>
<br>
And one also could think of expressions like<br>
<br>
foo = foo' (f x : T) y : Foo<br>
<br>
This will make programs a bit more readable.<br>
<br>
Regards,<br>
<br>
------<br>
Sergei<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>