@idrislang has them, too: https://github.com/idris-lang/Idris-dev/commit/180fc75336577d329d7e03a05d81f9d74c8e6000 …https://twitter.com/andreasdotorg/status/879770150475636736 …
The type distinguishes things which definitely consume and things which might not. You can only have a recursive rule after consuming.
-
-
BTW: that thing where F* uses Z3 to dissolve boring proofs is definitely worth stealing for Idris.
-
Gotta love that syntax of Z3!
- 9 more replies
New conversation -
-
-
Then, grammars may be infinite but parsers are guaranteed to consume. I need to write this up, as an exercise in totality in Idris.
-
The neat thing is that grammar definitions look more or less like parsec combinators. I'm boarding a plane now, so more on this later!
End of conversation
New conversation -
-
-
Very clever indeed! Looking forward to a more detailed documentation.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.