Struct Lean4File 

pub struct Lean4File {
    pub module_doc: Option<String>,
    pub imports: Vec<String>,
    pub opens: Vec<String>,
    pub declarations: Vec<Lean4Decl>,
}

A complete Lean 4 source file.

Fields

module_doc: Option<String>

Module documentation comment

imports: Vec<String>

Import statements: import Mathlib.Data.Nat.Basic

opens: Vec<String>

open statements: open Nat List

declarations: Vec<Lean4Decl>

Top-level declarations

Implementations

impl Lean4File

pub fn new() -> Self

Create a new empty Lean 4 file.

pub fn with_import(self, import: impl Into<String>) -> Self

Add a standard import.

pub fn with_open(self, open: impl Into<String>) -> Self

Add an open declaration.

pub fn add_decl(&mut self, decl: Lean4Decl)

Add a declaration.

pub fn emit(&self) -> String

Generate the complete Lean 4 source.

Trait Implementations

impl Clone for Lean4File

fn clone(&self) -> Lean4File

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Lean4File

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

Formats the value using the given formatter.

impl Default for Lean4File

fn default() -> Self

Returns the “default value” for a type.