[Agda] idiom brackets in 2.6.1
mechvel at scico.botik.ru
mechvel at scico.botik.ru
Wed Mar 18 14:32:17 CET 2020
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
More information about the Agda
mailing list