Struct GeneratedContract 

pub struct GeneratedContract {
    pub name: String,
    pub rust_assertions: String,
    pub lean_stubs: String,
    pub precondition_count: usize,
    pub postcondition_count: usize,
    pub lean_theorem_count: usize,
    pub invariant_count: usize,
}

Generated contract enforcement code for a single contract.

Fields

name: String

Contract name (from YAML filename stem).

rust_assertions: String

Generated Rust assertion functions.

lean_stubs: String

Generated Lean 4 theorem stubs (for unproved obligations).

precondition_count: usize

Number of preconditions generated.

postcondition_count: usize

Number of postconditions generated.

lean_theorem_count: usize

Number of Lean theorems linked.

invariant_count: usize

Number of invariant assertions generated.

Trait Implementations

impl Clone for GeneratedContract

fn clone(&self) -> GeneratedContract

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for GeneratedContract

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.