Enum Origin 

pub enum Origin {
    Authored,
    Helper {
        of: String,
    },
    Synthesized,
    Prelude,
}

Where a LOGOS declaration came from.

Variants

Authored

Written by the Lean author (or by Lean’s elaborator, as an exported declaration).

Helper

Introduced by the reader to preserve sharing inside the named authored declaration.

Fields

of: String

Synthesized

Synthesized with no single Lean counterpart (for example, a derived recursor).

Prelude

The LOGOS prelude’s own checked declaration of the same identity. It is not written in the document; the fresh context already holds it, and verification compares it all the same.

Trait Implementations

impl Clone for Origin

fn clone(&self) -> Origin

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Origin

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

Formats the value using the given formatter.

impl PartialEq for Origin

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

impl StructuralPartialEq for Origin