List of all items
Structs
- ActiveImplementationDescriptor
- AllowHostPrimitiveDecl
- AtpOptions
- AtpStatus
- AutomaticSequenceDecision
- CheckResult
- CoinductiveDecl
- ConstructorDecl
- ConvertOptions
- CoverageDiagnostic
- CoverageResult
- DefineClause
- DefineDecl
- Dependency
- Diagnostic
- Env
- EnvOptions
- EvalNatResult
- EvaluateOptions
- EvaluateResult
- Formalization
- FormalizationEvaluation
- FormalizationRequest
- FoundationDescriptor
- FoundationFrame
- FoundationReport
- InductiveDecl
- Interpretation
- Lambda
- ProofAssumption
- ProofAssumptionSnapshot
- ProofGoal
- ProofObject
- ProofObjectSnapshot
- ProofReport
- ProofReportDependency
- ProofReportVerdict
- ProofRule
- ProofRuleSnapshot
- ProofState
- RewriteOptions
- RewriteResult
- RootConstructDescriptor
- SimplifyOptions
- SimplifyResult
- Span
- StrictFoundationDecl
- SynthResult
- TacticOptions
- TacticRunResult
- TemplateDecl
- TerminationDiagnostic
- TerminationResult
- TotalityDiagnostic
- TotalityResult
- TraceEvent
- TruthTableEntry
- TruthTableRow
- check::CheckError
- check::CheckOk
- check::CheckResult
- cst_convert::RoundTripResult
- lean_export::LeanExportResult
- meta::MetaDiagnostic
- meta::MetatheoremCheck
- meta::MetatheoremReport
- meta::MetatheoremResult
- repl::Repl
- repl::ReplStep
- rocq::RocqExportError
Enums
- Aggregator
- AtpStatusKind
- CheckProofVerdict
- DefineMeasure
- EvalResult
- ExtractTarget
- FormalizationResultValue
- ModeFlag
- Node
- Op
- RewriteDirection
- RewriteOccurrence
- RunResult
- cst::CstNode
- meta::CheckKind
Functions
- automatic_sequences_domain_plugin
- build_corecursor_type
- build_dependency_graph
- build_eliminator_type
- build_proof
- check
- check::check_program
- check_proof_object
- classify_equality_rule
- compute_form_spans
- cst::clone_cst
- cst::cst_to_lino
- cst::lino_to_cst
- cst::print_cst
- cst_convert::parse_to_cst
- cst_convert::print_from_cst
- cst_convert::round_trip
- cst_js::parse_js
- cst_js::print_js
- cst_lean::parse_lean
- cst_lean::print_lean
- cst_rocq::parse_rocq
- cst_rocq::print_rocq
- cst_rust::parse_rust
- cst_rust::print_rust
- dec_round
- decide_automatic_sequence_theorem
- decode_anum
- desugar_hoas
- encode_anum
- equality_provenance_for_query
- eval_nat_term
- eval_node
- evaluate
- evaluate_file
- evaluate_formalization
- evaluate_with_env
- evaluate_with_options
- extract_literate_lino
- extract_program
- flatten_neutral_applies
- formalize_selected_interpretation
- format_diagnostic
- format_foundation_report
- format_proof_report
- format_trace_event
- format_trace_value
- goal_to_tptp
- is_convertible
- is_convertible_with_options
- is_covered
- is_num
- is_structurally_same
- is_terminating
- is_total
- key_of
- lean_export::export_lean
- lean_export::lean_ident
- match_proof_pattern
- meta::check_metatheorems
- meta::format_report
- nf
- nf_with_options
- parse_allow_host_primitive_form
- parse_atp_status
- parse_binding
- parse_bindings
- parse_coinductive_form
- parse_inductive_form
- parse_lino
- parse_one
- parse_proof_assumption_form
- parse_proof_object_form
- parse_rule_form
- parse_strict_foundation_form
- parse_tactic_links
- quantize
- register_coinductive
- register_inductive
- repl::format_env
- repl::run_repl
- rewrite
- rewrite_with_options
- rocq::export_rocq
- run
- run_tactics
- run_tactics_with_options
- run_typed
- scan_pure_links_offenders
- simplify
- simplify_with_options
- subst
- substitute
- synth
- tokenize_one
- whnf
- whnf_term
- whnf_with_options