Struct DeclarationInspectionFields 

pub struct DeclarationInspectionFields {
    pub source: bool,
    pub statement: bool,
    pub docstring: bool,
    pub attributes: bool,
    pub flags: bool,
    pub statement_pretty: bool,
    pub proof_search: bool,
}

Fields

source: bool

statement: bool

docstring: bool

attributes: bool

flags: bool

statement_pretty: bool

Render statement notation-aware (pp.universes false) when true, falling back to the raw term if the pretty-printer cannot render it; the fully-elaborated raw form when false.

proof_search: bool

Include proof-search-oriented facts such as simp/rw/instance/class. Defaults off because these facts may touch persistent extensions and lazy derived search indexes.

Trait Implementations

impl Clone for DeclarationInspectionFields

fn clone(&self) -> DeclarationInspectionFields

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Copy for DeclarationInspectionFields

impl Debug for DeclarationInspectionFields

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

Formats the value using the given formatter.

impl Default for DeclarationInspectionFields

fn default() -> Self

Returns the “default value” for a type.

impl Eq for DeclarationInspectionFields

impl<'lean> IntoLean<'lean> for DeclarationInspectionFields

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

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

impl PartialEq for DeclarationInspectionFields

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for DeclarationInspectionFields