List of all items

Structs

• CheckRef
• Checker
• CheckerCache
• SubtermCheckResult
• context::ContextBase
• context::ContextWrap
• facts::Fact
• facts::GlobalFacts
• facts::LocalFacts
• facts::TypeGuard
• hoas::HOASSymbols
• impls::CheckRefBranch
• impls::Trace
• impls::proving::GSPair
• impls::proving::GoalId
• impls::proving::GoalStateDebug
• impls::proving::PremiseId
• impls::proving::ProverState
• impls::proving::ProverStateI
• impls::proving::StratLine
• impls::proving::StrategiesDebug
• impls::proving::StrategyId
• impls::solving::Solutions
• impls::solving::Solvable
• paragraphs::ProofCheckState
• results::DocumentCheckResult
• results::TypeCheckResult
• rules::CommentRule
• rules::HOASRule
• rules::IsJudgmentRule
• rules::RuleSet
• rules::fixity::BinLRule
• rules::fixity::BinRRule
• rules::fixity::ConjunctiveRule
• rules::fixity::IsConjunctionRule
• rules::fixity::PairwiseConjunctiveRule
• rules::fixity::PrenexRule
• rules::fixity::ReorderRule
• rules::fixity::bin::BinLRule
• rules::fixity::bin::BinRRule
• rules::fixity::conj::ConjunctiveRule
• rules::fixity::conj::IsConjunctionRule
• rules::fixity::conj::PairwiseConjunctiveRule
• rules::fixity::pre::PrenexRule
• rules::fixity::reorder::ReorderRule
• rules::implicits::ImplicitRule
• rules::operators::bindin::BindInApplyRule
• rules::operators::bindin::BindInComputationRule
• rules::operators::bindin::BindInInferenceRule
• rules::operators::bindin::BindInInhabitableRule
• rules::operators::intersection::IntersectionTypeInhabitable
• rules::operators::letin::LetinComputation
• rules::operators::numbers::AdditionRule
• rules::operators::numbers::DivisionRule
• rules::operators::numbers::ExponentiationRule
• rules::operators::numbers::LessThan
• rules::operators::numbers::Logarithm
• rules::operators::numbers::Max
• rules::operators::numbers::MultiplicationRule
• rules::operators::numbers::NumberRule
• rules::operators::numbers::NumberTypes
• rules::operators::numbers::SubtractionRule
• rules::operators::pi::ApplyRule
• rules::operators::pi::ArrowRule
• rules::operators::pi::BetaRule
• rules::operators::pi::LambdaPiCheckingRule
• rules::operators::pi::LambdaPiInferenceRule
• rules::operators::pi::NeedsTypeRule
• rules::operators::pi::PiExtensionRule
• rules::operators::pi::PiInferenceRule
• rules::operators::pi::PiInhabitableRule
• rules::operators::pi::PiUniverseRule
• rules::operators::pi::PiVarianceRule
• rules::operators::typing::InferredTypeSimplificationRule
• rules::operators::typing::SimpleTypeOperatorRule
• rules::operators::typing::Subtyping
• rules::operators::universe::AnyRule
• rules::operators::universe::ComplexInhabitableRule
• rules::operators::universe::ComplexUniverseRule
• rules::operators::universe::SimpleInhabitableRule
• rules::operators::universe::SimpleUniverseRule
• rules::sequences::SeqConcatInferenceRule
• rules::sequences::SeqIndexRule
• rules::sequences::SeqInferenceRule
• rules::sequences::SeqUniverseRule
• rules::sequences::fold::Fold
• rules::sequences::fold::FoldInferenceRule
• rules::sequences::map::MapArgumentSimplificationRule
• rules::sequences::map::MapIndexSimplificationRule
• rules::sequences::map::MapInferenceRule
• rules::sequences::map::MapInhabitableRule
• rules::sequences::map::MapSimplificationRule
• rules::symbols::GenericBindPrep
• rules::symbols::GenericEquality
• rules::symbols::GenericInhabitable
• rules::symbols::GenericProof
• rules::symbols::GenericSimplification
• rules::symbols::GenericSubtyping
• rules::symbols::GenericTyping
• rules::symbols::GenericUniverse
• rules::unknowns::UnknownsRule
• split::CancelToken
• split::RayonSplit
• split::RayonStrategiesDepth
• split::RayonStrategiesOnly
• split::SingleThreadedSplit
• trace::ColorDisplay
• trace::Indent
• trace::results::DocumentCheckResult
• trace::results::TypeCheckResult
• utils::Ancestor
• utils::MutableRefList
• utils::RefList
• utils::RefListIter

Enums

• facts::GlobalOrLocal
• facts::GoalPremise
• impls::proving::GoalState
• impls::proving::Premise
• impls::solving::BoundedValue
• results::CheckResult
• results::ContentCheckResult
• results::ProofStepCheckResult
• results::ProofStepResult
• results::SymbolCheckResult
• rules::operators::numbers::NumberType
• rules::symbols::Premise
• trace::CheckLog
• trace::CheckLogCow
• trace::CheckingTask
• trace::Displayable
• trace::DisplayableRef
• trace::MessageLevel
• trace::PreCheckLog
• trace::RefCheckLog
• trace::results::CheckResult
• trace::results::ContentCheckResult
• trace::results::ProofStepCheckResult
• trace::results::ProofStepResult
• trace::results::SymbolCheckResult

Traits

• context::CowLike
• impls::solving::TermExtSolvable
• rules::CheckerRule
• rules::CheckingRule
• rules::ClonableDynCheckingRule
• rules::ClonableDynEqualityRule
• rules::ClonableDynInferenceRule
• rules::ClonableDynInhabitableRule
• rules::ClonableDynMarkerRule
• rules::ClonableDynPreparationRule
• rules::ClonableDynProofRule
• rules::ClonableDynSimplificationRule
• rules::ClonableDynSubtypeRule
• rules::ClonableDynUniverseRule
• rules::EqualityRule
• rules::InferenceRule
• rules::InhabitableRule
• rules::MarkerRule
• rules::PreparationRule
• rules::ProofRule
• rules::SimplificationRule
• rules::SizedSolverRule
• rules::SubtypeRule
• rules::UniverseRule
• rules::implicits::ImplicitExtApp
• rules::implicits::ImplicitExtBound
• rules::implicits::ImplicitExtTerm
• rules::symbols::GenericJudgment
• split::Cancellation
• split::SplitStrategy
• trace::CheckerRule
• trace::FmtTraceDisplay
• trace::SizedSolverRule
• trace::TraceDisplay
• utils::Merge

Macros

• rules::extractors::rules
• rules::operators::numbers::arith
• rules::operators::pi::ret
• rules::operators::pi::ret_i
• rules::rules
• rules::symbols::judg
• rules::symbols::uri
• trace::trace
• trace::traceref
• update

Functions

• check
• impls::backend::get_variable
• impls::equality::same_shape
• impls::preparation::get_path
• impls::solving::apply_solvable
• impls::solving::cleanup_cv
• impls::solving::is_solvable_id
• impls::solving::is_solvable_var
• rules::as_comment
• rules::extractors::addition
• rules::extractors::all_rule_extractors
• rules::extractors::all_symbol_extractors
• rules::extractors::any
• rules::extractors::apply
• rules::extractors::arrow_for
• rules::extractors::bind_in
• rules::extractors::binl
• rules::extractors::binr
• rules::extractors::conj
• rules::extractors::conjunction
• rules::extractors::division
• rules::extractors::exponentiation
• rules::extractors::hoas_lpa
• rules::extractors::implicit
• rules::extractors::inhab
• rules::extractors::inhabitable
• rules::extractors::intersection
• rules::extractors::judgment
• rules::extractors::lambda
• rules::extractors::leq
• rules::extractors::letrule
• rules::extractors::logarithm
• rules::extractors::map
• rules::extractors::max
• rules::extractors::multiplication
• rules::extractors::numcomplex
• rules::extractors::numint
• rules::extractors::numnat
• rules::extractors::numnegint
• rules::extractors::numnegrat
• rules::extractors::numnegreal
• rules::extractors::numnonzeroint
• rules::extractors::numnonzerorat
• rules::extractors::numnonzeroreal
• rules::extractors::numposnat
• rules::extractors::numposrat
• rules::extractors::numposreal
• rules::extractors::numrat
• rules::extractors::numreal
• rules::extractors::of_type
• rules::extractors::pi
• rules::extractors::prenex
• rules::extractors::prop
• rules::extractors::pwconj
• rules::extractors::reorder
• rules::extractors::subtp
• rules::extractors::subtraction
• rules::extractors::univ
• rules::extractors::universe
• rules::fixity::is_sequence_binary
• rules::fixity::match_head
• rules::fixity::was_sequence_binary
• rules::operators::intersection::intersect_pi_extension
• rules::operators::numbers::applicable
• rules::operators::pi::construct_binder
• rules::operators::pi::destruct_binder
• rules::sequences::is_index
• rules::symbols::parse
• rules::symbols::undo_implicits
• rules::unknowns::beta_unknowns
• rules::unknowns::beta_unknowns_cow
• rules::unknowns::unsolved
• topo_sort

Type Aliases

• BigSet
• rules::extractors::RuleExtractor
• rules::extractors::SymbolRuleExtractor

Statics

• CHECK
• DUMMY
• rules::sequences::fold::X
• rules::sequences::fold::Y
• rules::symbols::BINDS
• rules::symbols::DOC_URI
• rules::symbols::EQUAL
• rules::symbols::HAS_PROOF
• rules::symbols::HAS_TYPE
• rules::symbols::INH
• rules::symbols::NAMESPACE
• rules::symbols::SIMPLIFY
• rules::symbols::SUBTYPE
• rules::symbols::UNIV
• rules::symbols::URI

Constants

• context::CONTEXT_LEN
• impls::DEPTH_LIMIT
• impls::proving::MAX_DEPTH
• impls::simplify::LOOP_LIMIT
• impls::simplify::RECURSION_LIMIT
• impls::simplify::TOTAL_LIMIT
• impls::solving::PREFIX