List of all items

Structs

• args::Args
• context::Context
• database::Database
• elaborator::Elaborator
• occurrence_list::OccurrenceList
• order::ActiveOrder
• order::Order
• order_context::OrderContext
• order_context::ReflexivityContext
• order_context::SpecificationContext
• order_context::TransitivityContext
• parser::error::ParseError
• parser::lexer::Lexer
• parser::parser::Parser
• parser::utils::GenericTerms
• parser::utils::Position
• proofgoal::Proofgoal
• rules::AssumptionRule
• rules::Comment
• rules::ConclusionRule
• rules::DefineOrderRule
• rules::Deletion
• rules::DominanceBasedStrengtheningRule
• rules::EndProof
• rules::EndSubproof
• rules::EqualsObjectiveRule
• rules::EqualsRule
• rules::FailRule
• rules::FormulaCheck
• rules::HeaderRule
• rules::ImpliesRule
• rules::IsDeletedCheck
• rules::LoadOrderRule
• rules::MoveToCoreRule
• rules::ObjectiveUpdateRule
• rules::ObjectiveValueRule
• rules::OrderAuxVariablesRule
• rules::OrderDefConstraintRule
• rules::OrderDefRule
• rules::OrderFreshAux1Rule
• rules::OrderFreshAux2Rule
• rules::OrderFreshRightVariablesRule
• rules::OrderLeftVariablesRule
• rules::OrderProofRule
• rules::OrderReflexivityRule
• rules::OrderRightVariablesRule
• rules::OrderSpecificationRule
• rules::OrderTransitivityRule
• rules::OrderVariablesRule
• rules::OutputRule
• rules::PolRule
• rules::ProofByContradiction
• rules::ProofgoalRule
• rules::RUPRule
• rules::RedundanceBasedStrengtheningRule
• rules::ScopeRule
• rules::SetLevelRule
• rules::SolutionRule
• rules::StrengtheningToCoreRule
• rules::UnimplementedRule
• subproof_context::SubproofContext
• verifier::Verifier

Enums

• context::Subcontext
• deletion_sequence::DeletionSequenceEnum
• elaborator::ElaborationError
• error::CheckingError
• error::VeriPBError
• misc_tokens::IdentifierOption
• misc_tokens::IntegerOrSemicolonToken
• misc_tokens::IntegerToken
• misc_tokens::LiteralToken
• misc_tokens::OrderName
• misc_tokens::RUPHint
• misc_tokens::SubproofBeginToken
• misc_tokens::VariableToken
• order_context::OrderVariableKind
• parser::lexer::IntegerParseMode
• parser::utils::PolToken
• parser::utils::Scope
• parser::utils::Token
• proofgoal::ProofTechnique
• proofgoal::ProofgoalID
• rules::Bound
• rules::ConclusionResult
• rules::ConstraintDefRuleToken
• rules::DeletionOption
• rules::DeletionOrigin
• rules::Instruction
• rules::ObjectiveUpdateType
• rules::OutputGuarantee
• rules::OutputType
• rules::RuleToken
• rules::ScopeId
• rules::SolutionRuleOutput

Traits

• deletion_sequence::DeletionSequence
• rules::Rule

Functions

• database::move_to_derived_propagator
• rules::line_to_rule
• run_checker
• utils::check_implication
• utils::check_solution
• utils::check_substituted_implication
• utils::new_veripb_propagation_engine

Constants

• context::AUTOPROVING
• context::CORE
• context::DERIVED
• context::REQUIRED_RUP_STREAK