Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] NEWS: Isabelle/ML type Bytes.T and XZ comp...


view this post on Zulip Email Gateway (Jul 06 2022 at 13:46):

From: Makarius <makarius@sketis.net>
* ML *

This refers to Isabelle/44815dc2b8f9.

It might be occasionally useful to have XZ (un)compression available in
Isabelle/ML. XZ is the standard compression scheme of Isabelle/Scala.

The main point of the exercise, though, is to show how to implement this my
mostly trivial means, see:
https://isabelle.sketis.net/repos/isabelle/file/44815dc2b8f9/src/Pure/General/xz.ML
and
https://isabelle.sketis.net/repos/isabelle/file/44815dc2b8f9/src/Pure/General/xz.scala

A similar application is Base64 recoding in
https://isabelle.sketis.net/repos/isabelle/file/44815dc2b8f9/src/Pure/General/base64.ML
and
https://isabelle.sketis.net/repos/isabelle/file/44815dc2b8f9/src/Pure/General/base64.scala

Makarius


isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev


Last updated: Mar 04 2024 at 10:08 UTC