Re-exports§
pub use artifact::ArtifactBatch;pub use artifact::ArtifactLayout;pub use artifact::ArtifactRecord;pub use artifact::LEAN_MANIFEST_SCHEMA_VERSION;pub use artifact::LeanManifest;pub use artifact::LeanManifestAlias;pub use artifact::LeanManifestPrelude;pub use artifact::LeanManifestProject;pub use artifact::LeanManifestReportFiles;pub use artifact::LeanManifestTheorem;pub use artifact::dry_run_bundle_artifacts;pub use artifact::write_bundle_artifacts;pub use bundle::ObligationBundle;pub use command::CommandKind;pub use command::InvocationPlan;pub use command::KaniConfig;pub use command::LeanConfig;pub use command::LeanDriver;pub use command::SmtConfig;pub use export::export_lean_bundle;pub use export::export_lean_bundle_structured;pub use export::export_lean_bundle_structured_with_prelude;pub use export::export_lean_bundle_with_prelude;pub use export::export_smt_batch;pub use export::export_smt_bundle;pub use gpu::GpuObligationBundle;pub use gpu::IsBufferAlignedTo16;pub use gpu::IsDispatchWithinLimits;pub use gpu::IsMSLKernelDeterministic;pub use gpu::IsWorkgroupSizeDivisible;pub use kani::Kani;pub use kani::KaniHarness;pub use kani::export_kani_bundle;pub use kani::export_kani_harness;pub use lean::Lean4;pub use lean::LeanAlias;pub use lean::LeanExport;pub use lean::LeanImport;pub use lean::LeanPrelude;pub use lean::LeanProject;pub use lean::LeanTheorem;pub use lean::export;pub use lean::export_module as export_lean_module;pub use lean::export_module_with_prelude;pub use lean::export_with_prelude;pub use obligation::Declaration;pub use obligation::Obligation;pub use obligation::Origin;pub use obligation::ProofDialect;pub use obligation::Sort;pub use obligation::Term;pub use obligation::VerificationTier;pub use proof_bridge::ProofBridge;pub use proof_bridge::ProofEvidence;pub use report::ModuleReport;pub use report::ObligationReport;pub use report::VERIFICATION_REPORT_SCHEMA_VERSION;pub use report::VerificationReport;pub use report::dry_run_report;pub use report::execute_report;pub use runner::DryRunner;pub use runner::ExecutionResult;pub use runner::ExecutionStatus;pub use runner::LeanDiagnostic;pub use runner::LeanOutput;pub use runner::LocalProcessRunner;pub use runner::SmtOutput;pub use runner::VerificationPolicy;pub use runner::VerifierRunner;pub use runner::parse_lean_output;pub use runner::parse_smt_output;pub use runner::parse_smt_status;pub use session::DEFAULT_REPORT_STEM;pub use session::ReportFiles;pub use session::VERIFICATION_SIDECAR_SCHEMA_VERSION;pub use session::VerificationOutput;pub use session::VerificationSession;pub use session::verify_bundle;pub use session::verify_bundle_with_ci_outputs;pub use signature::AlgebraicSignature;pub use signature::BinarySymbol;pub use signature::ConstantSymbol;pub use signature::UnarySymbol;pub use smt::SmtLib2;pub use smt::export_obligation as export_smt_obligation;pub use trust::Certificate;pub use trust::Certified;pub use trust::ExternalTrust;pub use trust::KaniCertificate;pub use trust::LeanCertificate;pub use trust::ProofTestCertificate;pub use trust::SmtCertificate;pub use trust::VerificationBackend;
Modules§
Attribute Macros§
- export_
obligations - Export backend-agnostic verification obligations for an annotated item.