List of all items

Structs

• ast::DecisionBlock
• ast::FnDef
• ast::FnResolution
• ast::MatchArm
• ast::Module
• ast::TypeVariant
• ast::VerifyBlock
• ast::VerifyGiven
• ast::VerifyLaw
• checker::CheckFinding
• checker::ModuleCheckFindings
• checker::VerifyResult
• codegen::CodegenContext
• codegen::ModuleInfo
• codegen::ProjectOutput
• codegen::lean::ProofModeIssue
• config::EffectPolicy
• config::ProjectConfig
• interpreter::Interpreter
• interpreter::RecordingConfig
• interpreter::VerifyMatchCoverageMiss
• lexer::Lexer
• lexer::Token
• nan_value::Arena
• nan_value::ArenaUsage
• nan_value::NanValue
• parser::Parser
• replay::runtime::EffectReplayState
• replay::session::EffectRecord
• replay::session::SessionRecording
• runtime_bench_cases::CoreBenchCase
• tail_check::NonTailRecursionWarning
• types::checker::TypeCheckResult
• types::checker::TypeError
• value::FunctionValue
• verify_law::ContextualHelperLawHint
• verify_law::MissingHelperLawHint
• verify_law::NamedLawFunction
• verify_law::VerifyLawSpecRef
• vm::CallFrame
• vm::CodeStore
• vm::FnChunk
• vm::VM
• vm::VmBuiltinProfile
• vm::VmFunctionProfile
• vm::VmOpcodeProfile
• vm::VmProfileReport
• vm::VmReturnStats

Enums

• ast::BinOp
• ast::DecisionImpact
• ast::Expr
• ast::FnBody
• ast::Literal
• ast::Pattern
• ast::Stmt
• ast::StrPart
• ast::TopLevel
• ast::TypeDef
• ast::VerifyGivenDomain
• ast::VerifyKind
• codegen::lean::RecursionPlan
• codegen::lean::VerifyEmitMode
• interpreter::ExecutionMode
• lexer::LexerError
• lexer::TokenKind
• nan_value::AllocSpace
• nan_value::ArenaEntry
• nan_value::ArenaList
• nan_value::ArenaSymbol
• nan_value::NanString
• parser::ParseError
• replay::json::JsonValue
• replay::runtime::EffectReplayMode
• replay::runtime::ReplayFailure
• replay::session::RecordedOutcome
• types::Type
• value::EnvFrame
• value::RuntimeError
• value::Value
• vm::VmError

Functions

• call_graph::direct_calls
• call_graph::find_recursive_fns
• call_graph::find_tco_groups
• call_graph::ordered_fn_components
• call_graph::recursive_callsite_counts
• call_graph::recursive_scc_ids
• call_graph::tailcall_scc_components
• checker::check_module_intent
• checker::check_module_intent_with_sigs
• checker::check_module_intent_with_sigs_in
• checker::collect_verify_coverage_warnings
• checker::collect_verify_coverage_warnings_in
• checker::collect_verify_law_dependency_warnings
• checker::collect_verify_law_dependency_warnings_in
• checker::expr_to_str
• checker::index_decisions
• checker::merge_verify_blocks
• checker::run_verify
• codegen::build_context
• codegen::dafny::transpile
• codegen::lean::proof_mode_findings
• codegen::lean::proof_mode_issues
• codegen::lean::transpile
• codegen::lean::transpile_for_proof_mode
• codegen::lean::transpile_with_verify_mode
• codegen::rust::transpile
• effects::effect_satisfies
• format::try_format_source
• replay::json::first_diff_path
• replay::json::format_json
• replay::json::json_to_string
• replay::json::json_to_value
• replay::json::json_values_to_values
• replay::json::parse_json
• replay::json::value_to_json
• replay::json::value_to_json_lossy
• replay::json::values_to_json
• replay::json::values_to_json_lossy
• replay::session::parse_session_recording
• replay::session::session_recording_from_json
• replay::session::session_recording_to_json
• replay::session::session_recording_to_string_pretty
• resolver::resolve_program
• services::args::call
• services::args::call_nv
• services::args::effects
• services::args::register
• services::args::register_nv
• services::console::call
• services::console::call_nv
• services::console::effects
• services::console::register
• services::console::register_nv
• services::disk::call
• services::disk::call_nv
• services::disk::effects
• services::disk::register
• services::disk::register_nv
• services::env::call
• services::env::call_nv
• services::env::effects
• services::env::register
• services::env::register_nv
• services::http::call
• services::http::call_nv
• services::http::effects
• services::http::register
• services::http::register_nv
• services::http_server::call
• services::http_server::call_with_runtime
• services::http_server::effects
• services::http_server::register
• services::http_server::register_nv
• services::random::call
• services::random::call_nv
• services::random::effects
• services::random::register
• services::random::register_nv
• services::tcp::call
• services::tcp::call_nv
• services::tcp::effects
• services::tcp::register
• services::tcp::register_nv
• services::terminal::call
• services::terminal::call_nv
• services::terminal::effects
• services::terminal::register
• services::terminal::register_nv
• services::time::call
• services::time::call_nv
• services::time::effects
• services::time::register
• services::time::register_nv
• source::canonicalize_path
• source::find_module_file
• source::parse_source
• source::require_module_declaration
• tail_check::collect_non_tail_recursion_warnings
• tail_check::collect_non_tail_recursion_warnings_with_sigs
• tco::transform_program
• types::bool::call
• types::bool::call_nv
• types::bool::effects
• types::bool::register
• types::bool::register_nv
• types::byte::call
• types::byte::call_nv
• types::byte::effects
• types::byte::register
• types::byte::register_nv
• types::char::call
• types::char::call_nv
• types::char::effects
• types::char::register
• types::char::register_nv
• types::checker::run_type_check
• types::checker::run_type_check_full
• types::checker::run_type_check_with_base
• types::float::call
• types::float::call_nv
• types::float::effects
• types::float::register
• types::float::register_nv
• types::int::call
• types::int::call_nv
• types::int::effects
• types::int::register
• types::int::register_nv
• types::list::call
• types::list::call_nv
• types::list::effects
• types::list::register
• types::list::register_nv
• types::map::call
• types::map::call_nv
• types::map::effects
• types::map::register
• types::map::register_nv
• types::option::call
• types::option::call_nv
• types::option::effects
• types::option::extra_members
• types::option::register
• types::parse_type_str
• types::parse_type_str_strict
• types::result::call
• types::result::call_nv
• types::result::effects
• types::result::extra_members
• types::result::register
• types::string::call
• types::string::call_nv
• types::string::effects
• types::string::register
• types::string::register_nv
• types::vector::call
• types::vector::call_nv
• types::vector::effects
• types::vector::register
• types::vector::register_nv
• value::aver_display
• value::aver_repr
• value::hash_memo_args
• value::list_from_vec
• value::list_head
• value::list_len
• value::list_slice
• value::list_to_vec
• verify_law::canonical_spec_ref
• verify_law::canonical_spec_shape
• verify_law::collect_contextual_helper_law_hints
• verify_law::collect_missing_helper_law_hints
• verify_law::contextual_helper_law_message
• verify_law::declared_spec_ref
• verify_law::law_calls_function
• verify_law::law_spec_ref
• verify_law::missing_helper_law_message
• verify_law::named_law_function
• vm::compile_program
• vm::compile_program_with_modules
• vm::opcode::opcode_name
• vm::opcode::opcode_operand_width
• vm::register_service_types

Type Aliases

• nan_value::PersistentMap
• value::Env
• verify_law::FnSigMap

Constants

• runtime_bench_cases::CORE_BENCH_CASES
• vm::opcode::ADD
• vm::opcode::CALL_BUILTIN
• vm::opcode::CALL_KNOWN
• vm::opcode::CALL_LEAF
• vm::opcode::CALL_VALUE
• vm::opcode::CONCAT
• vm::opcode::DIV
• vm::opcode::DUP
• vm::opcode::EQ
• vm::opcode::EXTRACT_FIELD
• vm::opcode::EXTRACT_TUPLE_ITEM
• vm::opcode::GT
• vm::opcode::JUMP
• vm::opcode::JUMP_IF_FALSE
• vm::opcode::LIST_CONS
• vm::opcode::LIST_HEAD_TAIL
• vm::opcode::LIST_LEN
• vm::opcode::LIST_NEW
• vm::opcode::LIST_NIL
• vm::opcode::LIST_PREPEND
• vm::opcode::LOAD_CONST
• vm::opcode::LOAD_FALSE
• vm::opcode::LOAD_GLOBAL
• vm::opcode::LOAD_LOCAL
• vm::opcode::LOAD_LOCAL_2
• vm::opcode::LOAD_LOCAL_CONST
• vm::opcode::LOAD_TRUE
• vm::opcode::LOAD_UNIT
• vm::opcode::LT
• vm::opcode::MATCH_CONS
• vm::opcode::MATCH_DISPATCH
• vm::opcode::MATCH_DISPATCH_CONST
• vm::opcode::MATCH_FAIL
• vm::opcode::MATCH_NIL
• vm::opcode::MATCH_TAG
• vm::opcode::MATCH_TUPLE
• vm::opcode::MATCH_UNWRAP
• vm::opcode::MATCH_VARIANT
• vm::opcode::MOD
• vm::opcode::MUL
• vm::opcode::NEG
• vm::opcode::NOP
• vm::opcode::NOT
• vm::opcode::POP
• vm::opcode::PROPAGATE_ERR
• vm::opcode::RECORD_GET
• vm::opcode::RECORD_GET_NAMED
• vm::opcode::RECORD_NEW
• vm::opcode::RECORD_UPDATE
• vm::opcode::RETURN
• vm::opcode::STORE_GLOBAL
• vm::opcode::STORE_LOCAL
• vm::opcode::SUB
• vm::opcode::TAIL_CALL_KNOWN
• vm::opcode::TAIL_CALL_SELF
• vm::opcode::TAIL_CALL_SELF_THIN
• vm::opcode::TUPLE_NEW
• vm::opcode::UNWRAP_OR
• vm::opcode::UNWRAP_RESULT_OR
• vm::opcode::VARIANT_NEW
• vm::opcode::VECTOR_GET
• vm::opcode::VECTOR_GET_OR
• vm::opcode::VECTOR_SET
• vm::opcode::WRAP