Enum LeanMetaTransparency 

#[non_exhaustive]
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. #[non_exhaustive] so toolchain refinements can extend the taxonomy (e.g., a hypothetical None) without breaking exhaustive matches downstream.

Variants (Non-exhaustive)

Non-exhaustive enums could have additional variants added in future. Therefore, when matching against variants of non-exhaustive enums, an extra wildcard arm must be added to account for any future 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 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<'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<'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.

impl Copy for LeanMetaTransparency

impl Eq for LeanMetaTransparency

impl StructuralPartialEq for LeanMetaTransparency