Module types 

Types for the Proof Certificate System.

A proof certificate is a compact, checkable record that a term has been verified. Certificates enable exporting/importing proofs without re-checking from scratch.

Structs

CertificateStore

Persistent store of proof certificates, keyed by declaration name.

ProofCertId

Unique identifier for a proof certificate.

ProofCertificate

A compact verification record for a single declaration.

Enums

CertCheckResult

The result of checking a proof certificate against a live environment.

ProofStep

A single step in a proof reduction sequence.