<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body>Hi Sergei,<br><br>I haven't used them myself, but the documentation for idiom brackets is here: <a href="https://agda.readthedocs.io/en/v2.6.1/language/syntactic-sugar.html#idiom-brackets">https://agda.readthedocs.io/en/v2.6.1/language/syntactic-sugar.html#idiom-brackets</a> . They're probably more useful in programming than proving.<br><br>Regards,<br>James<br><br><div class="gmail_quote">On 18 March 2020 13:32:17 GMT, mechvel@scico.botik.ru wrote:<blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
<pre class="k9mail">Can anybody, please, explain what does it mean the following?<br><br>"<br> Idiom brackets can accommodate none or multiple applications separated <br>by a vertical bar `|`<br> if there are two additional operations<br> ```agda<br> empty : ∀ {A} → F A<br> _<|>_ : ∀ {A} → F A → F A → F A<br> ```<br> i.e. an Alternative type class in Haskell.<br>".<br><br>Please, give an example.<br>What is an Alternative type class in Haskell ? In Agda ?<br><br>Is it like this:<br><br> f :: (Foo1 a) -> a -> a<br><br> | (Foo2 a) -> a -> (a, a)<br><br>- to declare f having two signatures?<br><br>Thanks,<hr>Sergei<hr>Agda mailing list<br>Agda@lists.chalmers.se<br><a href="https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=02%7C01%7Cjames.wood.100%40strath.ac.uk%7Cdb12e08efccb4780914108d7cb40cb7e%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637201351459161057&sdata=vIvmJRfEwm2lwLRRKmRi%2BmEngLqzqRWEjpy2g81j5vc%3D&reserved=0">https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=02%7C01%7Cjames.wood.100%40strath.ac.uk%7Cdb12e08efccb4780914108d7cb40cb7e%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637201351459161057&sdata=vIvmJRfEwm2lwLRRKmRi%2BmEngLqzqRWEjpy2g81j5vc%3D&reserved=0</a><br></pre></blockquote></div><br>-- <br>Sent from my Android device with K-9 Mail. Please excuse my brevity.</body></html>