Enum Declaration 

pub enum Declaration {
    Inductive {
        name: String,
        params: Vec<String>,
        arity: Term,
        num_params: usize,
        ctors: Vec<(String, Term)>,
    },
    Definition {
        name: String,
        params: Vec<String>,
        ty: Term,
        body: Term,
    },
    Axiom {
        name: String,
        params: Vec<String>,
        ty: Term,
    },
    Quotient {
        primitives: Vec<(QuotKind, String, Vec<String>, Term)>,
        equality: String,
    },
    Observational {
        constants: Vec<(String, Vec<String>, Term)>,
        after: Vec<String>,
    },
}

A declaration as the core admits it, in the Term forms a Context registers. params are its universe parameters, in the order its constants take levels.

Variants

Inductive

One inductive family of a block: its arity (parameters included), how many of the arity’s binders are parameters, and each constructor’s full type.

Fields

name: String

params: Vec<String>

arity: Term

num_params: usize

ctors: Vec<(String, Term)>

Definition

Fields

name: String

params: Vec<String>

ty: Term

body: Term

Axiom

Fields

name: String

params: Vec<String>

ty: Term

Quotient

The quotient: its four primitives in the order the core admits them, installed together as Lean’s init_quot installs them, so a declaration that uses any of them sees the whole quotient and its computation rule. Each is checked against its canonical signature.

Fields

primitives: Vec<(QuotKind, String, Vec<String>, Term)>

equality: String

Observational

The certified observational equality’s constants (crate::observational), axioms to the core and computing by logos_obs, admitted together after after: every name the certificate rests on, which its rules’ answers are built from.

Fields

constants: Vec<(String, Vec<String>, Term)>

after: Vec<String>

Trait Implementations

impl Clone for Declaration

fn clone(&self) -> Declaration

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Declaration

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

Formats the value using the given formatter.