FStarLang / FStar

A Proof-oriented Programming Language
https://www.fstar-lang.org
Apache License 2.0
2.65k stars 232 forks source link

Functions in FStar.List.Pure are not in fstarlib #3312

Closed TWal closed 3 weeks ago

TWal commented 3 weeks ago

When compiling with OCaml a code that uses FStar.List.Pure.zip, we get the error:

Error: Unbound module FStar_List_Pure_Base

The reason seem to be that there is no file FStar_List_Pure_Base.ml in the fstar-lib snapshot: https://github.com/FStarLang/FStar/tree/master/ocaml/fstar-lib I have not digged further on why this file is excluded from the snapshot.