Struct LeanDeclarationFilter 

pub struct LeanDeclarationFilter {
    pub include_private: bool,
    pub include_generated: bool,
    pub include_internal: bool,
}

Lean-side declaration-listing filter.

The default is tuned for user-facing declaration browsers: include private names because callers may be indexing the current project, but drop compiler-generated and internal-detail names that usually swamp the list with implementation artifacts.

Fields

include_private: bool

Keep names Lean marks as private.

include_generated: bool

Keep generated names with numeric components.

include_internal: bool

Keep Lean internal-detail names such as _, match_, proof_, and similar implementation artifacts.

Trait Implementations

impl Clone for LeanDeclarationFilter

fn clone(&self) -> LeanDeclarationFilter

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LeanDeclarationFilter

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

Formats the value using the given formatter.

impl Default for LeanDeclarationFilter

fn default() -> Self

Returns the “default value” for a type.

impl<'lean> IntoLean<'lean> for LeanDeclarationFilter

fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean>

Allocate (or scalar-box) a Lean representation of self and return the owned handle.

impl<'lean> LeanAbi<'lean> for LeanDeclarationFilter

type CRepr = *mut lean_object

The C-ABI type Lake emits for this Lean type at function signatures.

impl PartialEq for LeanDeclarationFilter

fn eq(&self, other: &LeanDeclarationFilter) -> 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<'lean> TryFromLean<'lean> for LeanDeclarationFilter

fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self>

Decode obj into Self, returning a LeanError::Host with stage [HostStage::Conversion] if the object’s kind or payload is outside the type’s representable range.

impl Copy for LeanDeclarationFilter

impl Eq for LeanDeclarationFilter

impl SealedAbi for LeanDeclarationFilter

impl StructuralPartialEq for LeanDeclarationFilter