HomeIsabelle/Phabricator
Isabelle/ML type Bytes.T and XZ compression

ML

  • Type Bytes.T supports scalable byte strings, beyond the limit of String.maxSize (approx. 64 MB on 64_32 architecture).
  • Operations for XZ compression (via Isabelle/Scala):
XZ.compress: Bytes.T -> Bytes.T
XZ.uncompress: Bytes.T -> Bytes.T

This refers to Isabelle/44815dc2b8f9.

Written by makarius on Jul 6 2022, 3:38 PM.
User
Projects
None
Subscribers
None

Event Timeline