Struct Intake 

pub struct Intake { /* private fields */ }

An export that passed intake.

Implementations

impl Intake

pub fn header(&self) -> &Header

pub fn declarations(&self) -> &[Declaration]

Every declared constant, in export order — which lean4export makes dependency order.

pub fn declaration(&self, kernel_name: &str) -> Option<&Declaration>

The declaration registered under kernel_name.

pub fn closure(&self, kernel_name: &str) -> Result<Vec<String>, Verdict>

The dependency closure of kernel_name: the declaration itself, every constant its type and value mention, transitively, and every member of each inductive block reached — in export order, so the target comes after everything it depends on.

Trait Implementations

impl Debug for Intake

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

Formats the value using the given formatter.