package rocq-read-file
Read files from disk into Rocq primitive values
Install
Dune Dependency
Authors
Maintainers
Sources
v0.0.1.tar.gz
sha512=904f25c1b97e687b03edd9686572de0c9e44c3b74486e71692e455a5af13b3ebc4ef7bfb1dd14656c75c8c6457b111d7eaacbba929867cb60ac08ffe6796b1c5
Description
A Rocq plugin that reads binary files into Rocq-side primitive values: byte arrays, int63 arrays, or primitive strings. Auto-nests into primitive arrays when results exceed PArray.max_length.
Published: 18 May 2026
Dependencies (3)
-
ppx_optcomp
build -
dune
>= "3.8" & build -
ocaml
>= "4.14"
Dev Dependencies (3)
-
odoc
with-doc -
rocq-stdlib
>= "9.0" | = "dev" -
coq-core
>= "9.0" | = "dev"
Used by
None
Conflicts
None
On This Page