Alternative to Stream for total, recursive functions

Stream: lean4

[Matthew Toohey]

I'm working on a Protobuf library for Lean 4. It's still in the very early stages, and I'm working on varint support right now. I've managed to prove that my encoding functions are total, but because my decoding functions (for example: https://github.com/mtoohey31/lean4-protobuf/blob/c9dff0459a41e5fa78587fa1ece36d5d2708637a/Protobuf/Varint.lean#L17) operate recursively on streams, they're partial because there's no guarantee that a stream isn't endless.

Is there an alternative to Stream that has a similarly abstract next?-like method but also some notion of length that could be used to show termination? Thanks for any help!

[James Gallicchio]

was messing around with something like that a couple years ago, but I ended up not having a use for it so I never built a proper API for it. here's the last version I had (it's not much...): https://github.com/JamesGallicchio/LeanColls/blob/596d576cd6751e61cf521fe48e74d445a564f635/LeanColls/Stream.lean

[James Gallicchio]

and i'm excited for the protobuf library :D

[Matthew Toohey]

Awesome, SizedStream looks very promising so I'll try basing something off that. Thanks!