Enum LeanSessionImportProfile 

pub enum LeanSessionImportProfile {
    ExportedPublic,
    Server,
    Private,
    FullPrivateCompat,
}

Closed import profiles for full host sessions.

Profiles intentionally expose names tied to host semantics rather than raw Lean import knobs. All full-session profiles keep loadExts := true; the no-extension variant remains a profiling-only diagnostic path.

Variants

ExportedPublic

Public exported declarations only.

Server

Server-level import data without import all.

Private

Private-level import data without import all.

FullPrivateCompat

Legacy compatibility import shape: import all, private level, extensions loaded.

Implementations

impl LeanSessionImportProfile

pub const fn label(self) -> &'static str

pub const fn import_all(self) -> bool

pub const fn import_level(self) -> LeanImportLevel

pub const fn load_exts(self) -> bool

Trait Implementations

impl Clone for LeanSessionImportProfile

fn clone(&self) -> LeanSessionImportProfile

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Copy for LeanSessionImportProfile

impl Debug for LeanSessionImportProfile

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

Formats the value using the given formatter.

impl Default for LeanSessionImportProfile

fn default() -> LeanSessionImportProfile

Returns the “default value” for a type.

impl Eq for LeanSessionImportProfile

impl PartialEq for LeanSessionImportProfile

fn eq(&self, other: &LeanSessionImportProfile) -> 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 LeanSessionImportProfile