Alex Gryzlov
Alex Gryzlov
Sorry, I'm not related to development of Actario - simply found the link and thought it'd be relevant to share here :)
see WIP implementation at https://gitlab.com/thewalker77/ssrmap
https://gitlab.com/thewalker77/ssrmap
Can be based on * #10 * #8
- [x] #12 - [ ] #13 - [ ] #14 - [x] #15 - [x] #23
Isabelle: https://isa-afp.org/entries/Akra_Bazzi.html
Any chance this could be fixed in the future?
One thing that we definitely need for this to happen are the bounded versions (the analogue of Prelude's `Fin`), so that we could fix the byte length. This however will...