I'm playing around with the idea of allowing do bindings in expressions (à la Idris, Lean), and in modifying the parser to treat ← e as a special form I ran into the following __IMPOSSIBLE__:
postulate bind : _ syntax bind e (\ x -> f) = x \ e , f -- the '\' can also be any of 'let', 'do', '→', 'λ', wrapping 'e' in idiom brackets, etc
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at
src/full/Agda/Syntax/Notation.hs:224:26 in
Agda-2.8.0-4Mx4C0CQQ0476y2okW9iBX:Agda.Syntax.Notation
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