List of all items

Structs

• analysis::shape::Facts
• analysis::shape::FnRecognition
• analysis::shape::ProgramShape
• ast::AnnotBool
• ast::DecisionBlock
• ast::FnDef
• ast::FnResolution
• ast::MatchArm
• ast::Module
• ast::SourceSpan
• ast::Spanned
• ast::TailCallData
• ast::TypeVariant
• ast::VerifyBlock
• ast::VerifyGiven
• ast::VerifyLaw
• bench::DiffReport
• bench::MetricDiff
• bench::manifest::ExpectedShape
• bench::manifest::Manifest
• bench::manifest::Tolerance
• bench::report::BackendInfo
• bench::report::BenchReport
• bench::report::HostInfo
• bench::report::IterationStats
• bench::report::ScenarioMetadata
• checker::CheckFinding
• checker::FindingSpan
• checker::ModuleCheckFindings
• checker::VerifyCaseResult
• checker::VerifyLawContext
• checker::VerifyResult
• codegen::CodegenContext
• codegen::ModuleInfo
• codegen::ProjectOutput
• codegen::common::RefinementInfo
• codegen::lean::tactic_ir::InductionArm
• codegen::lemma_discovery::CommittedLemma
• codegen::program_view::ResolvedModuleFns
• codegen::program_view::ResolvedProgramView
• codegen::proof_lower::ProofLowerInputs
• codegen::recursion::ProofModeIssue
• codegen::rust::CoverageReport
• codegen::rust::MirEmitCtx
• codegen::rust::emit_ctx::EmitCtx
• config::CheckSuppression
• config::EffectPolicy
• config::ProjectConfig
• config::ShapeExpected
• config::ShapeLayerFingerprint
• diagnostics::analyze::AnalyzeOptions
• diagnostics::context::ContextDecisionSummary
• diagnostics::context::ContextFnSummary
• diagnostics::context::ContextSummary
• diagnostics::context::ContextTypeSummary
• diagnostics::context::FileContext
• diagnostics::model::AnalysisReport
• diagnostics::model::AnnotatedRegion
• diagnostics::model::Diagnostic
• diagnostics::model::FormatViolation
• diagnostics::model::RelatedSpan
• diagnostics::model::Repair
• diagnostics::model::SourceLine
• diagnostics::model::Span
• diagnostics::model::Underline
• diagnostics::model::VerifyBlockResult
• diagnostics::model::VerifySummary
• diagnostics::shape::CorpusSummary
• diagnostics::shape::FnShape
• diagnostics::shape::Histogram
• diagnostics::shape::LayerFingerprint
• diagnostics::shape::LayerVerdict
• diagnostics::shape::ModuleShape
• diagnostics::shape::RenderOptions
• diagnostics::shape::ShapeReport
• diagnostics::shape::VerifyReport
• diagnostics::why::DecisionSummary
• diagnostics::why::FnDetail
• diagnostics::why::WhySummary
• ir::AnalysisResult
• ir::BodyBindingPlan
• ir::BoolMatchShape
• ir::BufferBuildShape
• ir::DispatchArmPlan
• ir::DispatchDefaultPlan
• ir::DispatchTableShape
• ir::FnAnalysis
• ir::ForwardCallPlan
• ir::FusionSite
• ir::ListMatchShape
• ir::NeutralAllocPolicy
• ir::ThinBodyPlan
• ir::hir::ResolvedFnDef
• ir::hir::ResolvedMatchArm
• ir::hir::classify::ResolvedBodyBindingPlan
• ir::hir::classify::ResolvedForwardCallPlan
• ir::hir::classify::ResolvedThinBodyPlan
• ir::hir::resolve::ResolveCtx
• ir::identity::BuiltinId
• ir::identity::CtorId
• ir::identity::FnId
• ir::identity::FnKey
• ir::identity::LawKey
• ir::identity::ModuleId
• ir::identity::TypeId
• ir::identity::TypeKey
• ir::interval::Interval
• ir::interval::IntervalAnalysisResult
• ir::interval::RefinedTypeInterval
• ir::mir::expr::MirBinOp
• ir::mir::expr::MirCall
• ir::mir::expr::MirConstruct
• ir::mir::expr::MirEffectAnnotation
• ir::mir::expr::MirIfThenElse
• ir::mir::expr::MirIndependentProduct
• ir::mir::expr::MirLet
• ir::mir::expr::MirLocal
• ir::mir::expr::MirMatch
• ir::mir::expr::MirMatchArm
• ir::mir::expr::MirProject
• ir::mir::expr::MirRecordCreate
• ir::mir::expr::MirRecordField
• ir::mir::expr::MirRecordUpdate
• ir::mir::expr::MirTailCall
• ir::mir::instantiations::InstantiationRegistry
• ir::mir::optimize::bare_i64::BareI64Facts
• ir::mir::optimize::bare_i64::FnBareFacts
• ir::mir::optimize::bare_i64::ValueFact
• ir::mir::program::LocalId
• ir::mir::program::MirFn
• ir::mir::program::MirFnRepr
• ir::mir::program::MirParam
• ir::mir::program::MirProgram
• ir::mir::stats::LowerStats
• ir::pipeline::BuildSymbolsModule
• ir::pipeline::FnCountChange
• ir::pipeline::NonTailEntry
• ir::pipeline::PassDiagnostic
• ir::pipeline::PipelineConfig
• ir::pipeline::PipelineResult
• ir::proof_ir::EscapePairSpec
• ir::proof_ir::FloorDivShrink
• ir::proof_ir::FnContract
• ir::proof_ir::LawTheorem
• ir::proof_ir::NativeIntCountdownBody
• ir::proof_ir::Predicate
• ir::proof_ir::ProofIR
• ir::proof_ir::Quantifier
• ir::proof_ir::RefinedTypeDecl
• ir::proof_ir::SmartGuard
• ir::proof_ir::StringEscapeRoundtripPin
• ir::proof_ir::UnclassifiedFn
• ir::symbol_table::BuiltinEntry
• ir::symbol_table::CtorEntry
• ir::symbol_table::FnEntry
• ir::symbol_table::ModuleEntry
• ir::symbol_table::SymbolTable
• ir::symbol_table::TypeEntry
• lexer::Lexer
• lexer::Token
• nan_value::ArenaUsage
• nan_value::AverTypes
• nan_value::NanValue
• parser::Parser
• replay::runtime::EffectReplayState
• replay::session::EffectRecord
• replay::session::SessionRecording
• runtime_bench_cases::CoreBenchCase
• source::LoadedModule
• tail_check::NonTailRecursionWarning
• types::checker::TypeCheckResult
• types::checker::TypeError
• types::checker::TypeErrorSpan
• types::checker::effect_classification::EffectClassification
• types::checker::effect_lifting::LiftConfig
• types::checker::hostile_effects::HostileProfile
• value::FunctionValue
• verify_law::ContextualHelperLawHint
• verify_law::EntryFnIndex
• verify_law::FnSigInfo
• verify_law::MissingHelperLawHint
• verify_law::NamedLawFunction
• verify_law::VerifyLawSpecRef
• verify_law::expand::ExpandedCase
• visibility::ExportedTypeDef
• visibility::ModuleExports
• visibility::ModuleTypeDef
• visibility::SymbolEntry
• visibility::SymbolRegistry
• vm::CallFrame
• vm::CodeStore
• vm::FnChunk
• vm::VM
• vm::VmBuiltinProfile
• vm::VmFunctionProfile
• vm::VmOpcodeProfile
• vm::VmProfileReport
• vm::VmReturnStats
• vm::mir_vm::MirVmCoverage
• vm::runtime::TraceCoord

Enums

• analysis::shape::Archetype
• analysis::shape::ModulePattern
• ast::BinOp
• ast::DecisionImpact
• ast::Expr
• ast::FnBody
• ast::Literal
• ast::Pattern
• ast::Stmt
• ast::StrPart
• ast::TopLevel
• ast::TypeDef
• ast::VerifyGivenDomain
• ast::VerifyKind
• ast::types::Type
• bench::manifest::BenchTarget
• bench::manifest::ManifestError
• checker::VerifyCaseOutcome
• codegen::lean::VerifyEmitMode
• codegen::lean::tactic_ir::Tactic
• codegen::lemma_discovery::LemmaProvenance
• codegen::lemma_discovery::SimpDirection
• codegen::recursion::RecursionPlan
• config::IndependenceMode
• diagnostics::model::Severity
• diagnostics::shape::ApiShape
• diagnostics::shape::Bucket
• diagnostics::shape::CorpusEntry
• diagnostics::shape::Entry
• diagnostics::shape::Kind
• diagnostics::shape::Layer
• diagnostics::shape::Purity
• diagnostics::shape::StateShape
• diagnostics::shape::TypeSurface
• diagnostics::shape::VerifyLevel
• diagnostics::why::Justification
• ir::BodyExprPlan
• ir::BodyPlan
• ir::BodyShape
• ir::BoolCompareOp
• ir::BoolSubjectPlan
• ir::CallPlan
• ir::ConsumerKind
• ir::DispatchBindingPlan
• ir::DispatchLiteral
• ir::ForwardArg
• ir::LeafOp
• ir::MatchDispatchPlan
• ir::SemanticConstructor
• ir::SemanticDispatchPattern
• ir::TailCallPlan
• ir::ThinKind
• ir::WrapperKind
• ir::hir::BuiltinCtor
• ir::hir::BuiltinIntrinsic
• ir::hir::ResolvedCallee
• ir::hir::ResolvedCtor
• ir::hir::ResolvedExpr
• ir::hir::ResolvedFnBody
• ir::hir::ResolvedPattern
• ir::hir::ResolvedStmt
• ir::hir::ResolvedStrPart
• ir::hir::ResolvedTopLevel
• ir::hir::classify::ForwardSlot
• ir::hir::classify::ResolvedBodyExprPlan
• ir::hir::classify::ResolvedBodyPlan
• ir::hir::classify::ResolvedBoolSubjectPlan
• ir::hir::classify::ResolvedLeafOp
• ir::hir::classify::ThinKind
• ir::interval::Bound
• ir::interval::OpClass
• ir::mir::expr::MirCallee
• ir::mir::expr::MirCtor
• ir::mir::expr::MirExpr
• ir::mir::expr::MirPattern
• ir::mir::expr::MirStrPart
• ir::mir::optimize::bare_i64::Repr
• ir::mir::stats::SkipReason
• ir::pipeline::PassReport
• ir::pipeline::PipelineStage
• ir::pipeline::TypecheckMode
• ir::proof_ir::DecreaseProof
• ir::proof_ir::FloorWindowFigure
• ir::proof_ir::FuelMetric
• ir::proof_ir::MapUpdatePostconditionKind
• ir::proof_ir::Measure
• ir::proof_ir::PreservationProof
• ir::proof_ir::ProofStrategy
• ir::proof_ir::QuantifierType
• ir::proof_ir::RecursionContract
• ir::proof_ir::WrapperDriver
• lexer::LexerError
• lexer::TokenKind
• nan_value::AllocSpace
• nan_value::ArenaIntRef
• nan_value::ArenaList
• nan_value::NanString
• parser::ParseError
• replay::json::JsonValue
• replay::runtime::EffectReplayMode
• replay::runtime::ReplayFailure
• replay::session::RecordedOutcome
• types::checker::effect_classification::EffectDimension
• types::checker::effect_classification::RuntimeType
• types::checker::effect_lifting::LiftError
• value::EnvFrame
• value::RuntimeError
• value::Value
• verify_law::expand::ExpansionMode
• visibility::ModuleTypeKind
• visibility::SymbolKind
• vm::VmError
• vm::mir_vm::MirVmUnsupported
• vm::runtime::VmExecutionMode

Traits

• ir::AllocPolicy
• ir::CallLowerCtx
• ir::ThinBodyCtx
• nan_value::ArenaTypes
• nan_value::FnValueName
• nan_value::MapLike
• nan_value::NanIntExt
• nan_value::NanValueConvert
• verify_law::FnSigOracle

Functions

• analysis::shape::analyze_program
• analysis::shape::analyze_program_with_modules
• analysis::shape::classify
• analysis::shape::collect_inductable_sum_types
• analysis::shape::compute_sccs
• analysis::shape::detect_module_patterns
• analysis::shape::extract_facts
• analysis::shape::primary_label
• analysis::shape::type_is_result
• ast_rewrite::pattern_binding_names
• ast_rewrite::rewrite_idents_scoped
• bench::diff
• bench::format_diff
• bench::report::format_human
• bench::run_scenario
• 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_cse_warnings
• checker::collect_cse_warnings_in
• checker::collect_independence_warnings
• checker::collect_independence_warnings_in
• checker::collect_module_effects_warnings
• checker::collect_module_effects_warnings_in
• checker::collect_naming_warnings
• checker::collect_naming_warnings_in
• checker::collect_perf_warnings
• checker::collect_perf_warnings_in
• checker::collect_plain_cases_effectful_warnings
• checker::collect_plain_cases_effectful_warnings_in
• checker::collect_traversal_warnings_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
• codegen::build_context
• codegen::collect_verify_laws
• codegen::common::accumulator_fold_fn_names
• codegen::common::all_givens_are_singletons
• codegen::common::backend_named_type_key
• codegen::common::backend_type_def_key
• codegen::common::dafny_should_bound_accumulator_fold
• codegen::common::entry_basename
• codegen::common::find_fn_contract_for_fn
• codegen::common::find_fn_contract_scoped
• codegen::common::find_refined_type
• codegen::common::find_refined_type_by_id
• codegen::common::find_refined_type_for_named
• codegen::common::find_refined_type_scoped
• codegen::common::find_refined_type_with_key
• codegen::common::find_refined_type_with_key_scoped
• codegen::common::flatten_bool_and_conjuncts
• codegen::common::flatten_bool_and_conjuncts_resolved
• codegen::common::fn_contract_exists_for_fn
• codegen::common::fn_contract_exists_scoped
• codegen::common::fn_id_for_decl
• codegen::common::fn_id_for_dotted_name
• codegen::common::fn_key_for_decl
• codegen::common::fn_owning_scope_for
• codegen::common::is_pure_fn
• codegen::common::is_recursive_product
• codegen::common::is_recursive_sum
• codegen::common::is_recursive_type_def
• codegen::common::is_refinement_bool_ok_err_match
• codegen::common::law_calls_foreign_accumulator_fold
• codegen::common::law_calls_unclassified_fn
• codegen::common::law_lhs_has_trace_projection
• codegen::common::law_rhs_is_independent_of_givens
• codegen::common::nat_accfold_self_closeable
• codegen::common::predicate_syntactic_eq
• codegen::common::predicate_syntactic_eq_resolved
• codegen::common::project_lifted_idents_to_val
• codegen::common::refinement_info_for
• codegen::common::refinement_info_for_in_scope
• codegen::common::refinement_lift_for_given
• codegen::common::resolve_refined_type_in
• codegen::common::resolve_refined_type_in_with_key
• codegen::common::strip_refinement_wrappers
• codegen::common::substitute_ident_in_expr
• codegen::common::substitute_ident_in_resolved_expr
• codegen::common::swap_comparison_operands_op
• codegen::common::type_def_name
• codegen::common::type_key_for_decl
• codegen::common::type_key_for_name
• codegen::common::unclassified_fn_names
• codegen::common::verify_block_counter_key
• codegen::common::when_is_redundant_with_refinement_lifts
• codegen::dafny::transpile
• codegen::lean::count_model_panic_lines
• codegen::lean::proof_mode_findings
• codegen::lean::proof_mode_issues
• codegen::lean::residual_probe_body
• codegen::lean::tactic_ir::minimize::begin_collapse
• codegen::lean::tactic_ir::minimize::begin_instrument
• codegen::lean::tactic_ir::minimize::end
• codegen::lean::tactic_ir::minimize::parse_winners
• codegen::lean::tactic_ir::speculative::admits
• codegen::lean::tactic_ir::speculative::begin_probe
• codegen::lean::tactic_ir::speculative::clear
• codegen::lean::tactic_ir::speculative::parse_failures
• codegen::lean::tactic_ir::speculative::probed_ids
• codegen::lean::tactic_ir::speculative::probing
• codegen::lean::tactic_ir::speculative::record_probed
• codegen::lean::tactic_ir::speculative::set_committed
• codegen::lean::transpile
• codegen::lean::transpile_for_proof_mode
• codegen::lean::transpile_with_verify_mode
• codegen::lemma_discovery::apply_simp_over_lemma_pins
• codegen::lemma_discovery::discovery_surface_hash
• codegen::lemma_discovery::forbidden_token_in_lemma
• codegen::lemma_discovery::lemma_lhs_fns
• codegen::lemma_discovery::mentioned_fns
• codegen::lemma_discovery::parse_committed_lemmas
• codegen::lemma_discovery::plan_simp_over_lemma_pins
• codegen::lemma_discovery::simp_entries
• codegen::lemma_discovery::simp_orientation
• codegen::proof_lower::carrier_eligibility_demotions
• codegen::proof_lower::carrier_interval_table
• codegen::proof_lower::field_carrier_eligible_intervals
• codegen::proof_lower::field_carrier_interval_table
• codegen::proof_lower::lower
• codegen::proof_lower::populate_fn_contracts
• codegen::proof_lower::populate_law_theorems
• codegen::proof_lower::populate_refined_types
• codegen::recursion::detect::analyze_plans_in_scope
• codegen::recursion::detect::scc_has_growing_accumulator
• codegen::recursion::detect::sizeof_measure_param_indices
• codegen::recursion::expr_references_ident
• codegen::recursion::flip_comparison_binop
• codegen::recursion::fuel_helper_name
• codegen::recursion::native_aux_name
• codegen::recursion::rewrite_native_guarded_calls_body
• codegen::recursion::rewrite_native_guarded_calls_expr
• codegen::recursion::rewrite_native_guarded_calls_resolved_expr
• codegen::recursion::rewrite_recursive_calls_body
• codegen::recursion::rewrite_recursive_calls_expr
• codegen::rust::coverage_report
• codegen::rust::coverage_report_with_blockers
• codegen::rust::emit_ctx::expr_can_move
• codegen::rust::emit_ctx::expr_skip_clone
• codegen::rust::emit_ctx::is_copy_type
• codegen::rust::emit_ctx::should_borrow_param
• codegen::rust::transpile
• codegen::scc::analysis_set_to_fn_ids
• codegen::scc::bare_names_to_fn_ids
• diagnostics::analyze::analyze_source
• diagnostics::context::build_context_for_items
• diagnostics::context::render_context_md
• diagnostics::context::summarize
• diagnostics::factories::from_check_finding
• diagnostics::factories::from_type_error
• diagnostics::factories::needs_format_diagnostic
• diagnostics::factories::replay_effect_error_diagnostic
• diagnostics::factories::replay_output_mismatch_diagnostic
• diagnostics::factories::unused_binding_diagnostic
• diagnostics::factories::verify_mismatch_diagnostic
• diagnostics::factories::verify_runtime_error_diagnostic
• diagnostics::factories::verify_unexpected_err_diagnostic
• diagnostics::model::json_escape
• diagnostics::shape::analyze_dir
• diagnostics::shape::analyze_path
• diagnostics::shape::analyze_path_with
• diagnostics::shape::analyze_source_with
• diagnostics::shape::archetype_to_bucket
• diagnostics::shape::builtin_v0_layer_fingerprints
• diagnostics::shape::classify_layer
• diagnostics::shape::derive_kind
• diagnostics::shape::fingerprints_from_config
• diagnostics::shape::render_corpus_json
• diagnostics::shape::render_corpus_text
• diagnostics::shape::render_json
• diagnostics::shape::render_text
• diagnostics::shape::summarize_corpus
• diagnostics::verify_run::run_verify_blocks
• diagnostics::verify_run::run_verify_blocks_with_loaded
• diagnostics::verify_run::run_verify_blocks_with_loaded_and_mode
• diagnostics::verify_run::run_verify_blocks_with_mode
• diagnostics::vm_verify::run_verify_for_items_vm
• diagnostics::vm_verify::run_verify_for_items_vm_with_loaded
• diagnostics::vm_verify::run_verify_for_items_vm_with_loaded_and_mode
• diagnostics::vm_verify::run_verify_for_items_vm_with_mode
• diagnostics::why::summarize
• effects::effect_satisfies
• format::try_format_source
• ir::alias::annotate_program_alias_slots
• ir::analyze
• ir::classify_body_expr_plan
• ir::classify_body_plan
• ir::classify_bool_match_shape
• ir::classify_bool_match_shape_from_patterns
• ir::classify_bool_subject_plan
• ir::classify_call_plan
• ir::classify_callee
• ir::classify_constructor_name
• ir::classify_dispatch_pattern
• ir::classify_dispatch_table_shape
• ir::classify_dispatch_table_shape_from_patterns
• ir::classify_forward_call_parts
• ir::classify_forward_call_plan
• ir::classify_forward_fn_body
• ir::classify_leaf_op
• ir::classify_list_match_shape
• ir::classify_list_match_shape_from_patterns
• ir::classify_match_dispatch_plan
• ir::classify_match_dispatch_plan_from_patterns
• ir::classify_tail_call_plan
• ir::classify_thin_body_plan
• ir::classify_thin_fn_def
• ir::compute_alloc_info
• ir::compute_buffer_build_sinks
• ir::count_alloc_sites_in_fn
• ir::count_alloc_sites_in_program
• ir::dump::dump_items
• ir::escape::run
• ir::expr_to_dotted_name
• ir::find_fusion_sites
• ir::hir::classify::call_plan_from_resolved_callee
• ir::hir::classify::classify_body_expr_plan_resolved
• ir::hir::classify::classify_body_plan_resolved
• ir::hir::classify::classify_bool_match_shape_resolved
• ir::hir::classify::classify_bool_subject_plan_resolved
• ir::hir::classify::classify_dispatch_pattern_resolved
• ir::hir::classify::classify_dispatch_table_shape_resolved
• ir::hir::classify::classify_forward_call_resolved
• ir::hir::classify::classify_leaf_op_resolved
• ir::hir::classify::classify_list_match_shape_resolved
• ir::hir::classify::classify_match_dispatch_plan_resolved
• ir::hir::classify::classify_thin_fn_def_resolved
• ir::hir::classify::resolved_to_dotted
• ir::hir::classify::semantic_constructor_from_resolved_ctor
• ir::hir::count_unresolved_in_fn
• ir::hir::dump::dump_resolved_expr
• ir::hir::dump::dump_resolved_program
• ir::hir::resolve::resolve_fn_def_external
• ir::hir::resolve::resolve_program
• ir::hir::resolve::resolve_stmt_external
• ir::hir::resolve::resolve_top_level
• ir::interval::analyze
• ir::interval::classify_op
• ir::interval::interval_of_invariant
• ir::interval::raw_i64_eligible
• ir::is_builtin_namespace
• ir::last_use::annotate_program_last_use
• ir::lower_interpolation_pass
• ir::mir::instantiations::discover_instantiations
• ir::mir::lower::lower_program
• ir::mir::lower::lower_top_level_value
• ir::mir::optimize::algebraic::algebraic_simplify
• ir::mir::optimize::bare_i64::analyze
• ir::mir::optimize::bare_i64::analyze_with_fields
• ir::mir::optimize::bare_i64::type_is_int
• ir::mir::optimize::bare_i64_rewrite::mutual_recursion_box_set
• ir::mir::optimize::bare_i64_rewrite::rewrite_for_rust
• ir::mir::optimize::bare_i64_rewrite::rewrite_for_wasm_gc
• ir::mir::optimize::bool_match::bool_match_to_if
• ir::mir::optimize::branch_collapse::branch_collapse
• ir::mir::optimize::const_fold::const_fold
• ir::mir::optimize::dead_code::dead_code
• ir::mir::optimize::inline::inline_nullary_literals
• ir::mir::optimize::optimize
• ir::mir::optimize::own_param::own_param_refine
• ir::pipeline::buffer_build
• ir::pipeline::interp_lower
• ir::pipeline::last_use
• ir::pipeline::resolve
• ir::pipeline::run
• ir::pipeline::tco
• ir::pipeline::typecheck
• ir::rewrite_fusion_sites
• ir::run_buffer_build_pass
• ir::synthesize_buffered_variants
• ir::thin_body_plan_is_parent_thin_candidate
• ir::thin_kind_is_parent_thin_candidate
• ir::vars::collect_vars
• ir::vars::collect_vars_stmt
• ir::vars::pattern_bindings
• ir::vars::resolved_pattern_bindings
• replay::entry::encode_entry_args
• replay::entry::parse_entry_call
• replay::entry::recording_stem
• 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
• scc::mutually_recursive
• scc::tarjan_sccs
• services::all_effect_names
• 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::capture_output
• services::console::effects
• services::console::register
• services::console::register_nv
• services::console::write_stderr_plain_str
• services::console::write_stdout_str
• 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::load_compile_deps
• source::load_module_tree
• source::load_module_tree_from_map
• source::loaded_to_module_info
• 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
• tty_render::render_tty
• types::bool::call
• types::bool::call_nv
• types::bool::effects
• types::bool::register
• types::bool::register_nv
• types::branch_path::call_nv
• types::branch_path::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::effect_classification::classifications_for_proof_subset
• types::checker::effect_classification::classify
• types::checker::effect_classification::is_classified
• types::checker::effect_classification::is_verify_fabricable_handle
• types::checker::effect_classification::oracle_signature
• types::checker::effect_lifting::lift_body
• types::checker::effect_lifting::lift_fn_def
• types::checker::effect_lifting::lift_fn_def_with_helpers
• types::checker::effect_lifting::lower_pure_question_bang_fn
• types::checker::effect_lifting::oracle_params_for_effects
• types::checker::effect_lifting::type_to_annotation
• types::checker::hostile_effects::hostile_profiles_for
• types::checker::hostile_values::boundary_exprs
• types::checker::hostile_values::boundary_values
• types::checker::oracle_subtypes::has_bounded_subtype
• types::checker::run_type_check
• types::checker::run_type_check_full
• types::checker::run_type_check_full_self_host
• types::checker::run_type_check_with_base
• types::checker::run_type_check_with_loaded
• types::checker::run_type_check_with_loaded_self_host
• types::effect_event::register
• 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::map::set_nv_owned
• 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::trace::register
• types::vector::call
• types::vector::call_nv
• types::vector::effects
• types::vector::register
• types::vector::register_nv
• types::vector::vec_set_nv_owned
• value::aver_display
• value::aver_repr
• value::aver_repr_literal
• value::callable_declared_effects
• 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::expand::expand_law_cases
• verify_law::law_calls_function
• verify_law::law_spec_ref
• verify_law::missing_helper_law_message
• verify_law::named_law_function
• visibility::collect_all_module_symbols
• visibility::collect_module_exports
• visibility::collect_module_types
• visibility::is_exposed
• visibility::member_key
• visibility::module_decl
• visibility::qualified_member_key
• visibility::qualified_name
• vm::compile_program_with_loaded_modules
• vm::compile_program_with_mir_fallback
• vm::compile_program_with_modules
• vm::mir_vm::classify_mir_program_coverage
• vm::opcode::opcode_name
• vm::opcode::opcode_operand_width
• vm::register_service_types

Type Aliases

• ast::SourceLine
• ir::SemanticCallee
• ir::mir::optimize::bare_i64::CarrierIntervals
• ir::mir::optimize::bare_i64::FieldCarrierIntervals
• ir::pipeline::AfterPassHook
• nan_value::Arena
• nan_value::ArenaEntry
• nan_value::ArenaSymbol
• nan_value::PersistentMap
• value::Env
• verify_law::FnSigMap

Constants

• codegen::lean::LAW_CLASS_BOUNDED_DOMAIN
• codegen::lean::LAW_CLASS_MARKER_PREFIX
• codegen::lean::LAW_CLASS_UNIVERSAL
• codegen::lean::LEAN_PANIC_LINE_MARKER
• codegen::lean::PROOF_FUEL_EXHAUSTED_MSG
• codegen::recursion::OMEGA_PROOF_SENTINEL
• diagnostics::model::SCHEMA_VERSION
• diagnostics::vm_verify::VERIFY_HOSTILE_MAX_CASES
• nan_value::ARENA_REF_BIT
• nan_value::IMM_FALSE
• nan_value::IMM_TRUE
• nan_value::IMM_UNIT
• nan_value::INT_INLINE_MAX
• nan_value::INT_INLINE_MIN
• nan_value::SYMBOL_BUILTIN
• nan_value::SYMBOL_FN
• nan_value::SYMBOL_NAMESPACE
• nan_value::SYMBOL_NULLARY_VARIANT
• nan_value::TAG_ERR
• nan_value::TAG_IMMEDIATE
• nan_value::TAG_INLINE_VARIANT
• nan_value::TAG_INT
• nan_value::TAG_LIST
• nan_value::TAG_MAP
• nan_value::TAG_NONE
• nan_value::TAG_OK
• nan_value::TAG_RECORD
• nan_value::TAG_SOME
• nan_value::TAG_STRING
• nan_value::TAG_SYMBOL
• nan_value::TAG_TUPLE
• nan_value::TAG_VARIANT
• nan_value::TAG_VECTOR
• nan_value::WRAP_ERR
• nan_value::WRAP_OK
• nan_value::WRAP_SOME
• runtime_bench_cases::CORE_BENCH_CASES
• services::args::DECLARED_EFFECTS
• services::console::DECLARED_EFFECTS
• services::disk::DECLARED_EFFECTS
• services::env::DECLARED_EFFECTS
• services::http::DECLARED_EFFECTS
• services::http_server::DECLARED_EFFECTS
• services::random::DECLARED_EFFECTS
• services::tcp::DECLARED_EFFECTS
• services::terminal::DECLARED_EFFECTS
• services::time::DECLARED_EFFECTS
• types::branch_path::TYPE_NAME
• types::effect_event::FIELD_ARGS
• types::effect_event::FIELD_METHOD
• types::effect_event::FIELD_PATH
• types::effect_event::TYPE_NAME
• types::trace::FIELD_EVENTS
• types::trace::TYPE_NAME
• vm::opcode::ADD
• vm::opcode::ADD_FLOAT
• vm::opcode::ADD_INT
• vm::opcode::BUFFER_APPEND_SEP_UNLESS_FIRST
• vm::opcode::BUFFER_APPEND_STR
• vm::opcode::BUFFER_FINALIZE
• vm::opcode::BUFFER_NEW
• vm::opcode::CALL_BUILTIN
• vm::opcode::CALL_BUILTIN_OWNED
• vm::opcode::CALL_KNOWN
• vm::opcode::CALL_KNOWN_OWNED
• vm::opcode::CALL_LEAF
• vm::opcode::CALL_PAR
• vm::opcode::CALL_VALUE
• vm::opcode::CONCAT
• vm::opcode::DIV
• vm::opcode::DIV_FLOAT
• vm::opcode::DUP
• vm::opcode::EQ
• vm::opcode::EQ_INT
• vm::opcode::EXTRACT_FIELD
• vm::opcode::EXTRACT_TUPLE_ITEM
• vm::opcode::GT
• vm::opcode::GT_FLOAT
• vm::opcode::GT_INT
• vm::opcode::INT_DIV_EUCLID
• vm::opcode::INT_MOD_EUCLID
• 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::LT_FLOAT
• vm::opcode::LT_INT
• vm::opcode::MATCH_CONS
• vm::opcode::MATCH_DISPATCH
• vm::opcode::MATCH_DISPATCH_CONST
• vm::opcode::MATCH_FAIL
• vm::opcode::MATCH_INT_LITERAL
• 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::MOVE_LOCAL
• vm::opcode::MUL
• vm::opcode::MUL_FLOAT
• vm::opcode::MUL_INT
• vm::opcode::NEG
• vm::opcode::NEG_FLOAT
• vm::opcode::NEG_INT
• 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::SUB_FLOAT
• vm::opcode::SUB_INT
• 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::VECTOR_SET_OR_KEEP
• vm::opcode::WRAP