package alt-ergo-plugin-ab-why3
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
An experimental Why3 frontend for Alt-Ergo
Install
Dune Dependency
Authors
Maintainers
Sources
alt-ergo-2.6.2.tbz
sha256=39e2c9128a7d1e89f332e31a2716f359f3b9e1a925fe81f11fa4a749b5d24d82
sha512=ca953fe5a4964287de7e328ec4e3724a9baaa908c22862b075da5870bbf3707c7f78bd9fe0af98ee6c6382b5de0a4ddfcc93e09dc8b5b8e7d6ab6b1196a0656d
Description
An experimental front-end that parses a subset of Why3's logic. More precisely, this front-end targets proof obligations generated by the Atelier-B framework in Why3 format. It should be used with a prelude defining the B Set theory.
Published: 14 May 2025
Dependencies (4)
-
alt-ergo-parsers
= version -
alt-ergo-lib
= version -
alt-ergo
= version -
dune
>= "3.14"
Dev Dependencies (1)
-
odoc
with-doc
Used by
None
Conflicts (1)
On This Page