Skip to content

Releases: sr-lab/coqpyt

v1.0.0

18 Oct 16:11
@Nfsaavedra Nfsaavedra
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.
Compare
Choose a tag to compare
v1.0.0 Latest
Latest

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