OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo
https://alt-ergo.ocamlpro.com/
Other
132 stars 33 forks source link

Rewrite `Lib_usage` #1252

Open Halbaroth opened 1 month ago

Halbaroth commented 1 month ago

This issue is a remainder to rewrite the example Lib_usage after merging #1251. This module documented how to use the Alt-Ergo library with the legacy frontend. We cannot rewrite it now with Dolmen because a large part of the library logic with the Dolmen frontend is located in the Alt-Ergo binary and should be moved in the library. Writing a proper API for the Alt-Ergo library with the Dolmen AST as input has to be completed before explaining how to use it!