Struct LeanFile 

pub struct LeanFile {
    pub path: String,
    pub content: String,
}

A generated Lean 4 file.

Fields

path: String

Relative path within the Lean project (e.g. ProvableContracts/Defs/Softmax.lean).

content: String

Lean 4 source content.

Trait Implementations

impl Clone for LeanFile

fn clone(&self) -> LeanFile

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LeanFile

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

Formats the value using the given formatter.