Cvc.lean user manual

 Cvc.lean -- High-Level API for cvc5🔗

Adrien Champion

Cvc.lean is a high-level Lean 4 API for the cvc5 SMT solver, built on top of the lean-cvc5 Lean library. It adds a lot of quality of life features and strives to provide strong static guarantees. The following sections of this manual present the library in detail.

The Overview section showcases various features of cvc.lean to give an overview for newcomers to survey quickly. The rest of this document goes over the technical details needed to understand and use cvc.lean properly.

Contents

  1. 1. Overview
  2. 2. Environment
  3. 3. Sorts
  4. 4. Terms
  5. 5. The smt! Notation
  6. 6. Datatypes and Records
  7. 7. Solver
  8. 8. Proofs
  9. Index