1. Overview
This chapter gives a brief overview of cvc.lean's main features.
-
Terms discusses strongly-typed terms and the term DSL;
-
Solver presents basic solver interactions;
-
Symbols/States/Systems showcases a high-level part of cvc.lean that serves both as
-
an actual API for symbol/state/transition system representation and model-checking;
-
an example of the kind of high-level features one can build on top of cvc.lean.
-
-
Type-erased surveys the erased facet of cvc.lean which relaxes strong-typing so that terms/symbols/states/systems can be used without knowing at compile-time the type of the symbols manipulated. This is particularly useful when parsing end-user-defined terms/symbols/states/systems.