[Agda] idiom brackets in 2.6.1

[James Wood]

Hi Sergei,

I haven't used them myself, but the documentation for idiom brackets is here: https://agda.readthedocs.io/en/v2.6.1/language/syntactic-sugar.html#idiom-brackets . They're probably more useful in programming than proving.

Regards,
James

On 18 March 2020 13:32:17 GMT, mechvel at scico.botik.ru wrote:
>Can anybody, please, explain what does it mean the following?
>
>"
>Idiom brackets can accommodate none or multiple applications separated 
>by a vertical bar `|`
>   if there are two additional operations
>   ```agda
>   empty : ∀ {A} → F A
>   _<|>_ : ∀ {A} → F A → F A → F A
>   ```
>   i.e. an Alternative type class in Haskell.
>".
>
>Please, give an example.
>What is an Alternative type class in Haskell ?  In Agda ?
>
>Is it like this:
>
>   f :: (Foo1 a) -> a -> a
>
>        | (Foo2 a) -> a -> (a, a)
>
>- to declare  f  having two signatures?
>
>Thanks,
>
>------
>Sergei
>
>
>_______________________________________________
>Agda mailing list
>Agda at lists.chalmers.se
>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

-- 
Sent from my Android device with K-9 Mail. Please excuse my brevity.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200318/2512c334/attachment.html>