The Agda documentation on this webpage
https://agda.readthedocs.io/en/v2.6.2/language/syntax-declarations.html
has an example:syntax Σ A (λ x → B) = [ x ∈ A ] × B
Agda does not accept it. It generates the following error message:
Malformed syntax declaration: syntax must alternate holes (A x B) and non-holes ([ ∈ ] ×)
I believe the " ×" should be removed from the documentation.
I'm running Agda 2.6.0.1 on Ubuntu 20.04.3 LTS.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4