Struct WellKnown 

pub struct WellKnown {

    pub nat: NameId,
    pub nat_zero: NameId,
    pub nat_succ: NameId,
    pub nat_add: NameId,
    pub nat_sub: NameId,
    pub nat_mul: NameId,
    pub nat_pow: NameId,
    pub nat_gcd: NameId,
    pub nat_mod: NameId,
    pub nat_div: NameId,
    pub nat_beq: NameId,
    pub nat_ble: NameId,
    pub nat_land: NameId,
    pub nat_lor: NameId,
    pub nat_xor: NameId,
    pub nat_shift_left: NameId,
    pub nat_shift_right: NameId,
    pub nat_pred: NameId,
    pub nat_bitwise: NameId,
    pub bool_: NameId,
    pub bool_true: NameId,
    pub bool_false: NameId,
    pub string: NameId,
    pub string_of_list: NameId,
    pub char_: NameId,
    pub char_of_nat: NameId,
    pub list_nil: NameId,
    pub list_cons: NameId,
    pub list: NameId,
    pub eq: NameId,
    pub quot: NameId,
    pub quot_mk: NameId,
    pub quot_lift: NameId,
    pub quot_ind: NameId,
    pub installed_quot: Option<QuotNames>,
    pub logos_true: Option<NameId>,
    pub eager_reduce: NameId,
    pub opt_param: NameId,
    pub auto_param: NameId,
    pub out_param: NameId,
    pub semi_out_param: NameId,
    pub nested_prefix: NameId,
    pub u: NameId,
}

Fields

nat: NameId

nat_zero: NameId

nat_succ: NameId

nat_add: NameId

nat_sub: NameId

nat_mul: NameId

nat_pow: NameId

nat_gcd: NameId

nat_mod: NameId

nat_div: NameId

nat_beq: NameId

nat_ble: NameId

nat_land: NameId

nat_lor: NameId

nat_xor: NameId

nat_shift_left: NameId

nat_shift_right: NameId

nat_pred: NameId

nat_bitwise: NameId

bool_: NameId

bool_true: NameId

bool_false: NameId

string: NameId

string_of_list: NameId

char_: NameId

char_of_nat: NameId

list_nil: NameId

list_cons: NameId

list: NameId

eq: NameId

quot: NameId

quot_mk: NameId

quot_lift: NameId

quot_ind: NameId

installed_quot: Option<QuotNames>

A second quotient the theory admits beside its own: under LOGOS’s theory, the one a kernel installs (kernel.quot.*, quotient::Kind’s names) for content imported from Lean.

logos_true: Option<NameId>

The theory’s own true beside the primitives’ Bool.true, where they differ: LOGOS’s true, read by the decide fast path (Kernel::is_true_constant).

eager_reduce: NameId

opt_param: NameId

auto_param: NameId

out_param: NameId

semi_out_param: NameId

nested_prefix: NameId

u: NameId

Implementations

impl WellKnown

pub fn new(n: &mut Names) -> WellKnown

pub fn logos(n: &mut Names) -> WellKnown

The same meanings in a LOGOS context. LOGOS’s own constants keep its spelling: Nat, Zero/Succ, Eq and the quotient’s Quot_mk/Quot_lift/Quot_ind, its true read by the decide fast path. A meaning only Lean content has (the Nat operations, Bool, Char, String, List, the elaborator’s markers) is spelled as the Lean importer names it in a LOGOS context (dag::name::kernel_name_of_components), so an imported Nat.div is the primitive it is, checked and computed as in Lean’s theory.

pub fn quot_names(&self) -> QuotNames

The theory’s own quotient.

pub fn primitives(&self) -> [NameId; 24]

The names Lean’s kernel treats as primitive: declaring one is only allowed in its canonical form.

Trait Implementations

impl Clone for WellKnown

fn clone(&self) -> WellKnown

Returns a duplicate of the value.

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

Performs copy-assignment from source.