Enum LeanMetaTransparency 

pub enum LeanMetaTransparency {
    Default,
    Reducible,
    Instances,
    All,
}

Reducibility setting threaded into the bounded MetaM runner.

Maps 1-1 onto Lean’s Meta.TransparencyMode at 4.29.1. Declaration order doubles as the on-wire byte the Lean shim reads; the Self::as_byte accessor exposes that contract for the dispatch site.

Variants

Default

Lean’s standard reducibility—non-reducible / non-irreducible definitions unfold on demand.

Reducible

Only @[reducible] definitions unfold. Useful when you want crate::host::meta::whnf to expose the surface structure of a term without diving into expensive bodies.

Instances

Default plus the bodies of instance bindings.

All

Every definition unfolds. Most aggressive setting—also the most likely to blow the heartbeat budget on non-trivial terms.

Implementations

impl LeanMetaTransparency

pub fn as_byte(self) -> u8

On-wire byte the Lean shim’s transparencyOfByte reads.

Trait Implementations

impl Clone for LeanMetaTransparency

fn clone(&self) -> LeanMetaTransparency

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Copy for LeanMetaTransparency

impl Debug for LeanMetaTransparency

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

Formats the value using the given formatter.

impl Default for LeanMetaTransparency

fn default() -> LeanMetaTransparency

Returns the “default value” for a type.

impl Eq for LeanMetaTransparency

impl<'lean> IntoLean<'lean> for LeanMetaTransparency

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 LeanMetaTransparency

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

impl<'lean> TryFromLean<'lean> for LeanMetaTransparency

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.