Re-exports§
pub use error::Error;pub use error::Result;pub use syntax::lexer;pub use syntax::lexer::Lexer;pub use typing::Typed;pub use typing::TypeChecker;pub use typing::TypeRef;pub use typing::GroundTypeRef;pub use client::Client;pub use location::*;
Modules§
Structs§
- Binding
- Variable binding.
- Constructor
Declaration - Context
- Evaluation context. Maps each variable to its sort.
- Data
Type Declaration - Data type declaration.
- Ground
Sort - A ground sort is a sort fully applied (arity 0).
- Match
Case - Selector
Declaration - Selector declaration.
- Sort
Declaration - Sort declaration.
- Sorted
- Sorted
Var - Sorted variable.
- Unresolved
Constructor Declaration - Unresolved
Data Type Declaration - Data type declaration.
- Unresolved
Selector Declaration - Selector declaration, where sorts are unresolved references.
Enums§
- Abstract
Ground Sort - A ground sort with sort parameter variables, used in a datatype declaration. Parameters are identified with their index.
- Command
- SMT2-lib command.
- Pattern
- Term
- A term.
- Type
Check Error - Functions type check errors.
Traits§
- Compiler
- Environment
- SMT2-lib solver environment.
- Function
- SMT2-lib function.
- Server
- Sorted
With
Functions§
- compile
- compile_
binding - compile_
constructor_ declaration - compile_
datatype_ declaration - compile_
function - compile_
ident - compile_
selector_ declaration - compile_
sort - compile_
sort_ declaration - compile_
sort_ ref - compile_
sorted_ var - compile_
symbol - compile_
term