List of all items

Structs

• environment::Environment
• environment::KnownFnInfo
• environment::KnownForallFactParamsAndDom
• error::ArithmeticRuntimeError
• error::DefineParamsRuntimeError
• error::InferRuntimeError
• error::InstantiateRuntimeError
• error::NameAlreadyUsedRuntimeError
• error::NewFactRuntimeError
• error::ParseRuntimeError
• error::RuntimeErrorStruct
• error::StoreFactRuntimeError
• error::UnknownRuntimeError
• error::VerifyRuntimeError
• error::WellDefinedRuntimeError
• fact::AndFact
• fact::ChainFact
• fact::EqualFact
• fact::ExistFactBody
• fact::FnEqualFact
• fact::FnEqualInFact
• fact::ForallFact
• fact::ForallFactWithIff
• fact::GreaterEqualFact
• fact::GreaterFact
• fact::InFact
• fact::IsCartFact
• fact::IsFiniteSetFact
• fact::IsNonemptySetFact
• fact::IsSetFact
• fact::IsTupleFact
• fact::LessEqualFact
• fact::LessFact
• fact::NormalAtomicFact
• fact::NotEqualFact
• fact::NotForallFact
• fact::NotGreaterEqualFact
• fact::NotGreaterFact
• fact::NotInFact
• fact::NotIsCartFact
• fact::NotIsFiniteSetFact
• fact::NotIsNonemptySetFact
• fact::NotIsSetFact
• fact::NotIsTupleFact
• fact::NotLessEqualFact
• fact::NotLessFact
• fact::NotNormalAtomicFact
• fact::NotRestrictFact
• fact::NotSubsetFact
• fact::NotSupersetFact
• fact::OrFact
• fact::RestrictFact
• fact::SubsetFact
• fact::SupersetFact
• infer::InferResult
• module_manager::ModuleManager
• obj::Abs
• obj::Add
• obj::AnonymousFn
• obj::ByInducFreeParamObj
• obj::Cap
• obj::Cart
• obj::CartDim
• obj::Choose
• obj::ClosedRange
• obj::Count
• obj::Cup
• obj::DefAlgoFreeParamObj
• obj::DefHeaderFreeParamObj
• obj::Div
• obj::ExistFreeParamObj
• obj::FamilyObj
• obj::FiniteSeqListObj
• obj::FiniteSeqSet
• obj::FnObj
• obj::FnSet
• obj::FnSetBody
• obj::FnSetFreeParamObj
• obj::ForallFreeParamObj
• obj::Identifier
• obj::IdentifierWithMod
• obj::Intersect
• obj::ListSet
• obj::Log
• obj::MatrixAdd
• obj::MatrixListObj
• obj::MatrixMul
• obj::MatrixPow
• obj::MatrixScalarMul
• obj::MatrixSet
• obj::MatrixSub
• obj::Max
• obj::Min
• obj::Mod
• obj::Mul
• obj::Number
• obj::ObjAtIndex
• obj::Pow
• obj::PowerSet
• obj::Product
• obj::Proj
• obj::Range
• obj::SeqSet
• obj::SetBuilder
• obj::SetBuilderFreeParamObj
• obj::SetDiff
• obj::SetMinus
• obj::Sub
• obj::Sum
• obj::Tuple
• obj::TupleDim
• obj::Union
• parse::TokenBlock
• result::FactualStmtSuccess
• result::NonFactualStmtSuccess
• result::StmtUnknown
• runtime::FreeParamCollection
• runtime::FreeParamTypeAndLineFile
• runtime::runtime::Runtime
• stmt::ByEnumerateClosedRangeStmt
• stmt::by_stmt::ByCasesStmt
• stmt::by_stmt::ByContraStmt
• stmt::by_stmt::ByEnumerateFiniteSetStmt
• stmt::by_stmt::ByExtensionStmt
• stmt::by_stmt::ByFamilyStmt
• stmt::by_stmt::ByFnSetStmt
• stmt::by_stmt::ByFnStmt
• stmt::by_stmt::ByForStmt
• stmt::by_stmt::ByInducStmt
• stmt::by_stmt::ByTupleStmt
• stmt::claim_stmt::ClaimStmt
• stmt::define_algorithm_stmt::AlgoCase
• stmt::define_algorithm_stmt::AlgoReturn
• stmt::define_algorithm_stmt::DefAlgoStmt
• stmt::definition_stmt::DefAbstractPropStmt
• stmt::definition_stmt::DefFamilyStmt
• stmt::definition_stmt::DefLetStmt
• stmt::definition_stmt::DefPropStmt
• stmt::definition_stmt::FnSetClause
• stmt::definition_stmt::HaveByExistStmt
• stmt::definition_stmt::HaveFnByInducNestedCase
• stmt::definition_stmt::HaveFnByInducStmt
• stmt::definition_stmt::HaveFnEqualCaseByCaseStmt
• stmt::definition_stmt::HaveFnEqualStmt
• stmt::definition_stmt::HaveObjEqualStmt
• stmt::definition_stmt::HaveObjInNonemptySetOrParamTypeStmt
• stmt::eval_stmt::EvalStmt
• stmt::know_stmt::KnowStmt
• stmt::parameter_def::FiniteSet
• stmt::parameter_def::NonemptySet
• stmt::parameter_def::ParamDefWithType
• stmt::parameter_def::ParamGroupWithParamType
• stmt::parameter_def::ParamGroupWithSet
• stmt::parameter_def::Set
• stmt::prove_stmt::ProveStmt
• stmt::tooling_stmt::ClearStmt
• stmt::tooling_stmt::DoNothingStmt
• stmt::tooling_stmt::ImportGlobalModuleStmt
• stmt::tooling_stmt::ImportRelativePathStmt
• stmt::tooling_stmt::RunFileStmt
• stmt::witness_stmt::WitnessExistFact
• stmt::witness_stmt::WitnessNonemptySet
• verify::VerifyState

Enums

• common::json_value::JsonValue
• error::RuntimeError
• fact::AndChainAtomicFact
• fact::AtomicFact
• fact::ChainAtomicFact
• fact::ExistBodyFact
• fact::ExistFactEnum
• fact::ExistOrAndChainAtomicFact
• fact::Fact
• fact::OrAndChainAtomicFact
• obj::AtomObj
• obj::AtomicName
• obj::FnObjHead
• obj::FnSetSpace
• obj::Obj
• obj::ParamObjType
• obj::StandardSet
• result::StmtResult
• stmt::Stmt
• stmt::by_stmt::ClosedRangeOrRange
• stmt::define_algorithm_stmt::AlgoReturnOrAlgoCase
• stmt::definition_stmt::HaveFnByInducLastCase
• stmt::parameter_def::ParamType
• stmt::tooling_stmt::ImportStmt
• verify::NumberCompareResult

Functions

• builtin_code::builtin_code
• cli::run_cli
• common::count_range_integer::count_closed_range_integer_endpoints
• common::count_range_integer::count_half_open_range_integer_endpoints
• common::defaults::default_line_file
• common::defaults::is_default_line_file
• common::helper::add_four_spaces_at_beginning
• common::helper::brace_vec_colon_vec_to_string
• common::helper::braced_string
• common::helper::braced_vec_to_string
• common::helper::comma_separated_stored_fn_params_as_user_source
• common::helper::curly_braced_vec_to_string
• common::helper::curly_braced_vec_to_string_with_sep
• common::helper::is_number_string_literally_integer_without_dot
• common::helper::remove_windows_carriage_return
• common::helper::to_string_and_add_four_spaces_at_beginning_of_each_line
• common::helper::todo_error_message
• common::helper::vec_pair_to_string
• common::helper::vec_to_string_add_four_spaces_at_beginning_of_each_line
• common::helper::vec_to_string_join_by_comma
• common::helper::vec_to_string_with_sep
• common::is_valid_litex_name::is_valid_litex_name
• common::json_value::json_one_level_indent
• common::json_value::json_string_literal
• common::json_value::line_file_line_json_fragment
• common::json_value::line_file_line_json_value
• common::json_value::line_file_source_json_fragment
• common::json_value::line_file_source_json_value
• common::json_value::render_json_value
• common::keywords::is_builtin_identifier_name
• common::keywords::is_builtin_predicate
• common::keywords::is_comparison_str
• common::keywords::is_key_symbol_or_keyword
• common::keywords::is_keyword
• common::keywords::key_symbols_sorted_by_len_desc
• error::short_exec_error
• fact::check_anonymous_fn_has_no_duplicate_fn_set_free_parameter
• fact::check_exist_fact_has_no_duplicate_exist_free_parameter
• fact::check_fn_set_has_no_duplicate_fn_set_free_parameter
• fact::check_forall_fact_has_no_duplicate_forall_free_parameter
• fact::check_forall_fact_with_iff_has_no_duplicate_forall_free_parameter
• fact::check_set_builder_has_no_duplicate_set_builder_free_parameter
• obj::fn_obj_to_string
• obj::identifier_to_string
• obj::identifier_with_mod_to_string
• obj::obj_for_bound_param_in_scope
• obj::param_binding_element_obj_for_store
• obj::strip_free_param_numeric_tags_in_display
• obj::strip_parsing_free_param_tags_for_user_display
• parse::tokenize_line
• pipeline::display_runtime_error_json
• pipeline::display_stmt_exec_result_json
• pipeline::pipeline::render_run_source_code_output
• pipeline::pipeline::run_source_code
• pipeline::pipeline::run_source_code_in_file
• pipeline::pipeline::run_source_code_in_file_with_ok
• pipeline::pipeline_repl::run_repl
• pipeline::pipeline_run_stmt_globally::run_stmt_at_global_env
• rational_expression::mul_signed_decimal_str
• rational_expression::normalize_decimal_number_string
• rational_expression::objs_equal_by_rational_expression_evaluation
• stmt::definition_stmt::induc_obj_plus_offset
• to_latex::to_latex
• to_latex::to_latex_from_source_after_builtins
• verify::compare_normalized_number_str_to_zero
• verify::number_is_in_n
• verify::number_is_in_n_pos
• verify::number_is_in_q_neg
• verify::number_is_in_q_nz
• verify::number_is_in_q_pos
• verify::number_is_in_r_neg
• verify::number_is_in_r_nz
• verify::number_is_in_r_pos
• verify::number_is_in_z
• verify::number_is_in_z_neg
• verify::number_is_in_z_nz

Type Aliases

• common::defaults::LineFile
• common::name_types::AbstractPropName
• common::name_types::AlgoName
• common::name_types::AtomicFactKey
• common::name_types::ExistFactKey
• common::name_types::FactString
• common::name_types::FamilyName
• common::name_types::IdentifierName
• common::name_types::ObjString
• common::name_types::OrFactKey
• common::name_types::PropName

Constants

• builtin_code::common_comparison_properties::BUILTIN_ENV_CODE_FOR_COMMON_COMPARISON_PROPERTIES
• builtin_code::common_comparison_properties::KNOW_ORDER_TRANSITIVITY_CHAIN
• builtin_code::common_comparison_properties::KNOW_REAL_LINE_TRICHOTOMY
• builtin_code::common_comparison_properties::ORDER_TRANSITIVITY_PROP_DECLS
• builtin_code::common_facts::COMMON_FACTS
• builtin_code::common_functions::BUILTIN_ENV_CODE_FOR_COMMON_FUNCTIONS
• builtin_code::fundamental_comparison::BUILTIN_ENV_CODE_FOR_FUNDAMENTAL_COMPARISON
• builtin_code::fundamental_number_properties::FUNDAMENTAL_NUMBER_PROPERTIES
• builtin_code::set_operators::BUILTIN_ENV_CODE_FOR_SET_OPERATORS
• common::defaults::DEFAULT_MANGLED_FN_PARAM_PREFIX
• common::defaults::FILE_INDEX_FOR_BUILTIN
• common::keywords::ABS
• common::keywords::ABSTRACT_PROP
• common::keywords::ADD
• common::keywords::ALGO
• common::keywords::AND
• common::keywords::ANONYMOUS_FN_PREFIX
• common::keywords::AS
• common::keywords::BY
• common::keywords::CAP
• common::keywords::CART
• common::keywords::CART_DIM
• common::keywords::CASE
• common::keywords::CASES
• common::keywords::CHOOSE
• common::keywords::CLAIM
• common::keywords::CLEAR
• common::keywords::CLOSED_RANGE
• common::keywords::COLON
• common::keywords::COMMA
• common::keywords::CONTRA
• common::keywords::COUNT
• common::keywords::CUP
• common::keywords::DIV
• common::keywords::DOT_AKA_FIELD_ACCESS_SIGN
• common::keywords::DOT_DOT_DOT
• common::keywords::DOUBLE_QUOTE
• common::keywords::DO_NOTHING
• common::keywords::END_STRATEGY
• common::keywords::ENUMERATE
• common::keywords::EQUAL
• common::keywords::EQUIVALENT_SIGN
• common::keywords::EVAL
• common::keywords::EXIST
• common::keywords::EXIST_BANG
• common::keywords::EXTENSION
• common::keywords::FACT_PREFIX
• common::keywords::FAMILY
• common::keywords::FAMILY_OBJ_PREFIX
• common::keywords::FINITE_SEQ
• common::keywords::FINITE_SET
• common::keywords::FN_EQ
• common::keywords::FN_EQ_IN
• common::keywords::FN_LOWER_CASE
• common::keywords::FOR
• common::keywords::FORALL
• common::keywords::FORALL_BANG
• common::keywords::FROM
• common::keywords::GREATER
• common::keywords::GREATER_EQUAL
• common::keywords::HAVE
• common::keywords::IMPORT
• common::keywords::IMPOSSIBLE
• common::keywords::IN
• common::keywords::INDUC
• common::keywords::INDUC_PARAM_2_NAME
• common::keywords::INFIX_FN_NAME_SIGN
• common::keywords::INTERSECT
• common::keywords::IS_CART
• common::keywords::IS_FINITE_SET
• common::keywords::IS_NONEMPTY_SET
• common::keywords::IS_SET
• common::keywords::IS_TUPLE
• common::keywords::KNOW
• common::keywords::LEFT_BRACE
• common::keywords::LEFT_BRACKET
• common::keywords::LEFT_CURLY_BRACE
• common::keywords::LESS
• common::keywords::LESS_EQUAL
• common::keywords::LET
• common::keywords::LOG
• common::keywords::MATRIX
• common::keywords::MATRIX_ADD
• common::keywords::MATRIX_MUL
• common::keywords::MATRIX_POW
• common::keywords::MATRIX_SCALAR_MUL
• common::keywords::MATRIX_SUB
• common::keywords::MAX
• common::keywords::MIN
• common::keywords::MOD
• common::keywords::MOD_SIGN
• common::keywords::MUL
• common::keywords::N
• common::keywords::NONEMPTY_SET
• common::keywords::NOT
• common::keywords::NOT_EQUAL
• common::keywords::N_POS
• common::keywords::OR
• common::keywords::POW
• common::keywords::POWER_SET
• common::keywords::PRODUCT
• common::keywords::PROJ
• common::keywords::PROP
• common::keywords::PROVE
• common::keywords::Q
• common::keywords::Q_NEG
• common::keywords::Q_NZ
• common::keywords::Q_POS
• common::keywords::R
• common::keywords::RANGE
• common::keywords::RESTRICTIVE
• common::keywords::RESTRICT_FN_IN
• common::keywords::RIGHT_ARROW
• common::keywords::RIGHT_BRACE
• common::keywords::RIGHT_BRACKET
• common::keywords::RIGHT_CURLY_BRACE
• common::keywords::RUN_FILE
• common::keywords::R_NEG
• common::keywords::R_NZ
• common::keywords::R_POS
• common::keywords::SEQ
• common::keywords::SET
• common::keywords::SET_DIFF
• common::keywords::SET_MINUS
• common::keywords::ST
• common::keywords::STRATEGY
• common::keywords::STRONG_INDUC
• common::keywords::STRUCT
• common::keywords::SUB
• common::keywords::SUBSET
• common::keywords::SUCCESS_COLON
• common::keywords::SUM
• common::keywords::SUPERSET
• common::keywords::TUPLE
• common::keywords::TUPLE_DIM
• common::keywords::UNION
• common::keywords::UNKNOWN_COLON
• common::keywords::USE_STRATEGY
• common::keywords::WITNESS
• common::keywords::Z
• common::keywords::Z_NEG
• common::keywords::Z_NZ
• module_manager::BUILTIN_CODE_PATH