List of all items
Structs
- BigInt
- Context
- MutualInductive
- StructInfo
- cc::EGraph
- cc::UnionFind
- elaborate::MetaCtx
- inductive_compile::Compiled
- inductive_compile::IsoNames
- inductive_compile::NestedDecl
- inductive_compile::NestedInfo
- interface::Repl
- interface::TermParser
- lia::Constraint
- lia::LinearExpr
- lia::Rational
- omega::IntConstraint
- omega::IntExpr
- prelude::StandardLibrary
- reify::VarInterner
- ring::Monomial
- ring::Polynomial
Enums
- KernelError
- Literal
- Term
- Universe
- cc::ENode
- elaborate::ParamKind
- interface::Command
- interface::InterfaceError
- interface::ParseError
- lia::LiaError
- recheck::DoubleCheck
- recheck::ReCheckError
- ring::ReifyError
- simp::STerm
Functions
- bitvector::reflection_certificate
- bitvector::reflection_symmetry_proven
- bitvector::rev_n
- cc::check_goal
- cc::decompose_goal
- cc::reify
- check_positivity_for_test
- defeq_for_test
- elaborate::auto_bind_implicits
- elaborate::bind_self_recursion
- elaborate::elaborate
- elaborate::elaborate_anon_ctor
- elaborate::elaborate_app
- elaborate::elaborate_app_against
- elaborate::elaborate_dot
- elaborate::elaborate_in
- elaborate::fill_match_motives
- elaborate::instantiate
- elaborate::is_meta
- elaborate::resolve_coercion
- elaborate::resolve_instance
- elaborate::surface_elaborate
- elaborate::surface_elaborate_against
- elaborate::unify
- elaborate::unify_in
- eval::eval_bool
- eval::eval_bool_tree
- eval::native_compile_bool
- eval::native_compile_decide
- eval::native_decide
- field_algebra::conditional_subtract_in_range
- field_algebra::gauss_three_multiply_identity
- field_algebra::mldsa_montgomery_congruence
- field_algebra::mldsa_montgomery_divisibility
- field_algebra::mldsa_montgomery_reduction_certified
- field_algebra::montgomery_reduction_certified
- field_algebra::montgomery_reduction_congruence
- field_algebra::montgomery_reduction_divisibility
- inductive_compile::compile_nested
- infer_type
- instantiate_universes
- int_lit
- 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
- lit_bigint
- normalize
- omega::extract_comparison
- omega::goal_to_negated_constraint
- omega::omega_unsat
- omega::reify_int_linear
- positivity::check_positivity
- positivity::check_positivity_mutual
- recheck::double_check
- recheck::recheck
- recursor::derive_recursor
- ring::reify
- simp::check_goal
- termination::check_termination
- termination::check_termination_mutual
- word_ring::add_associative
- word_ring::add_commutative
- word_ring::additive_identity
- word_ring::all_word_ring_laws_certified
- word_ring::karatsuba_expand
- word_ring::left_distributive
- word_ring::mul_associative
- word_ring::mul_commutative
- word_ring::multiplicative_identity