Enum Transparency 

pub enum Transparency<'a> {
    All,
    Excluding(&'a (dyn Fn(&str) -> bool + Sync)),
}

The δ-transparency axis (Lean’s TransparencyMode): normalize_at/normalize_checked_at keep an @[irreducible] constant folded with its body intact, while normalize stays the kernel’s own always-unfolding setting. How much δ a reduction is allowed — Lean’s TransparencyMode, narrowed to the axis that actually changes the answer.

FOLLOWING LEAN, INCLUDING WHERE IT IS SUBTLE. Reducibility in Lean is an ELABORATOR attribute: Lean’s KERNEL unfolds every definition whatever its attribute, which is why example : secret = 5 := rfl on an @[irreducible] def secret : Nat := 5 is refused by the elaborator and accepted by the kernel. So Transparency::All is the kernel’s own setting and stays what normalize uses, and Transparency::Excluding is the elaborator’s default transparency — the setting under which an @[irreducible] constant keeps its body AND stays folded. Collapsing the two in either direction is a real loss: always-transparent makes LOGOS prove by rfl what Lean’s elaborator refuses (the over-permissive direction), and routing irreducibility through add_declaration instead throws the body away and manufactures a silent axiom.

The opacity set is supplied as a PREDICATE rather than read out of the Context, so the reducer does not have to know how the attribute is stored: a reducibility map in Context wires in as Transparency::Excluding(&|n| ctx.is_irreducible(n)) and nothing here changes.

Variants

All

Unfold every definition. The kernel’s setting.

Excluding(&'a (dyn Fn(&str) -> bool + Sync))

Keep every constant the predicate accepts FOLDED, body intact. The elaborator’s default.

+ Sync is not decoration: without it Transparency is not Send, and a normalisation entry point that cannot cross a thread boundary cannot be run on a SIZED STACK — which is what stops a deep term ABORTING the process instead of failing. The bound costs nothing: every predicate here is built from Context::is_irreducible, and Context is Sync.

Trait Implementations

impl<'a> Clone for Transparency<'a>

fn clone(&self) -> Transparency<'a>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<'a> Copy for Transparency<'a>