Skip to content

v1.0.0

Latest
Latest
Compare
Choose a tag to compare
@Nfsaavedra Nfsaavedra released this 18 Oct 16:11
v1.0.0
35ebaaa
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Learn about vigilant mode.

We are thrilled to announce the release of CoqPyt v1.0.0!

Key Features:

  • Seamless Interaction with Coq Files: Easily execute Coq files and retrieve generated contexts, including terms, tactics, and notations.
  • Proof Exploration: Access current goals, proof steps, and contexts interactively, making it easier to automate proof development.
  • Proof Management: Create, edit, and manipulate proof files using an intuitive API. Add or remove proof steps dynamically, with built-in support for handling proof context and goals.
  • Batch Proof Changes: Apply proof modifications transactionally with automatic rollback on errors, ensuring consistent proof states.
  • Execution and Compilation: Run proofs step-by-step or execute complete files.
  • Coq versions: CoqPyt currently supports Coq versions 8.17, 8.18, 8.19, and 8.20 depending on the coq-lsp version you use.
  • Coq Equations: CoqPyt supports the special terms defined in the plugin Coq Equations.
Assets 2
Loading