Struct LeanProject 

pub struct LeanProject {
    pub package_name: String,
    pub toolchain: String,
    pub requires_mathlib: bool,
}

Generated Lean package metadata for writing a runnable project scaffold.

Fields

package_name: String

toolchain: String

requires_mathlib: bool

Implementations

impl LeanProject

pub fn new(package_name: impl Into<String>) -> Self

pub fn for_export(export: &LeanExport) -> Self

pub fn with_toolchain(self, toolchain: impl Into<String>) -> Self

pub fn with_mathlib(self, requires_mathlib: bool) -> Self

pub fn render_lakefile(&self) -> String

pub fn render_toolchain(&self) -> String

Trait Implementations

impl Clone for LeanProject

fn clone(&self) -> LeanProject

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LeanProject

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

Formats the value using the given formatter.

impl Eq for LeanProject

impl PartialEq for LeanProject

fn eq(&self, other: &LeanProject) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for LeanProject