High-level, strongly-typed API for the cvc5 SMT solver built on top of lean-cvc5.

NB: cvc.lean will not build unless you run a lake update ... command such as lake update cvc.

• Documentation
• Depending on cvc.lean
• Build

Documentation

• API documentation (WIP)
• User Manual (WIP)

Depending on cvc.lean

Cvc.lean is not on reservoir yet, you must depend on the git repository explicitly.

Toml lakefile:

[[require]]
name = "cvc"
git = "https://github.com/anzenlang/cvc.lean"

Lean lakefile:

require cvc from git "https://github.com/anzenlang/cvc.lean"

Build

To build this library directly or as a dependency, make sure you first run lake update cvc to make sure this library's main dependency, lean-cvc5, builds properly.