Enum EnvironmentEntry 

pub enum EnvironmentEntry {
    Axiom {
        name: String,
        level_params: Vec<String>,
        ty: NodeRef,
    },
    Definition {
        name: String,
        level_params: Vec<String>,
        ty: NodeRef,
        body: NodeRef,
    },
    Theorem {
        name: String,
        level_params: Vec<String>,
        ty: NodeRef,
        proof: NodeRef,
    },
    Opaque {
        name: String,
        level_params: Vec<String>,
        ty: NodeRef,
        body: NodeRef,
    },
    Inductive {
        level_params: Vec<String>,
        types: Vec<InductiveType>,
    },
    Structure {
        inductive: String,
        projections: Vec<String>,
    },
    Quotient {
        primitive: QuotientPrimitive,
        level_params: Vec<String>,
        ty: NodeRef,
        equality: Option<String>,
    },
}

One declaration of an environment, in dependency order.

Variants

Axiom

An assumption: a name and a type, no proof. Subject to the reader’s assumption policy.

Fields

name: String

level_params: Vec<String>

ty: NodeRef

Definition

A transparent definition, δ-unfoldable. Recursors and structure projections are definitions: their bodies are type-checked like any other.

Fields

name: String

level_params: Vec<String>

ty: NodeRef

body: NodeRef

Theorem

A theorem. Its proof is carried and checked by both kernels, and the declaration is published as Lean publishes a theorem: conversion may unfold it at the lowest priority.

Fields

name: String

level_params: Vec<String>

ty: NodeRef

proof: NodeRef

Opaque

A checked opaque value or proof. Its body is evidence and never unfolds in conversion.

Fields

name: String

level_params: Vec<String>

ty: NodeRef

body: NodeRef

Inductive

An inductive block (one member, or a mutual block) and its constructors.

Fields

level_params: Vec<String>

types: Vec<InductiveType>

Structure

Structure η for an earlier single-constructor inductive, through earlier projection definitions. Registered only after every projection is proved to compute.

Fields

inductive: String

projections: Vec<String>

Quotient

A certified quotient primitive. equality names the equality inductive lift respects.

Fields

primitive: QuotientPrimitive

level_params: Vec<String>

ty: NodeRef

equality: Option<String>

Implementations

impl EnvironmentEntry

pub fn names(&self) -> Vec<&str>

The names this entry introduces, in order.

pub fn roots(&self) -> Vec<NodeRef>

Every term row this entry cites directly.

Trait Implementations

impl Clone for EnvironmentEntry

fn clone(&self) -> EnvironmentEntry

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for EnvironmentEntry

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for EnvironmentEntry

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl PartialEq for EnvironmentEntry

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

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for EnvironmentEntry