List of all items
Structs
- Context
- cc::EGraph
- cc::UnionFind
- interface::Repl
- interface::TermParser
- lia::Constraint
- lia::LinearExpr
- lia::Rational
- omega::IntConstraint
- omega::IntExpr
- prelude::StandardLibrary
- ring::Monomial
- ring::Polynomial
Enums
- KernelError
- Literal
- Term
- Universe
- cc::ENode
- interface::Command
- interface::InterfaceError
- interface::ParseError
- lia::LiaError
- ring::ReifyError
- simp::STerm
Functions
- cc::check_goal
- cc::decompose_goal
- cc::reify
- infer_type
- interface::literate_parser::parse_definition
- interface::literate_parser::parse_inductive
- interface::literate_parser::parse_let_definition
- interface::literate_parser::parse_theorem
- interface::parse_command
- is_subtype
- lia::extract_comparison
- lia::fourier_motzkin_unsat
- lia::goal_to_negated_constraint
- lia::reify_linear
- normalize
- omega::extract_comparison
- omega::goal_to_negated_constraint
- omega::omega_unsat
- omega::reify_int_linear
- positivity::check_positivity
- ring::reify
- simp::check_goal
- termination::check_termination