Skip to main content

Compiled

logicaffeine_kernel::inductive_compile

Struct Compiled

pub struct Compiled {
    pub block: Vec<MutualInductive>,
    pub isos: Vec<(String, Term, Term)>,
    pub iso_names: Vec<IsoNames>,
    pub siblings: Vec<String>,
}

Expand description

The compiled artifacts of a nested inductive: the mutual block to register, and the iso DEFINITIONS (name, type, body) to kernel-check and add. Nothing here is trusted until the caller checks it.

Fields§

§block: Vec<MutualInductive>§isos: Vec<(String, Term, Term)>§iso_names: Vec<IsoNames>§siblings: Vec<String>

Auto Trait Implementations§

impl Freeze for Compiled

impl RefUnwindSafe for Compiled

impl Send for Compiled

impl Sync for Compiled

impl Unpin for Compiled

impl UnsafeUnpin for Compiled

impl UnwindSafe for Compiled

Blanket Implementations§

impl<T> Any for T
where T: 'static + ?Sized,

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more

impl<T> Borrow<T> for T
where T: ?Sized,

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more

impl<T> BorrowMut<T> for T
where T: ?Sized,

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more

impl<T> From<T> for T

fn from(t: T) -> T

Returns the argument unchanged.

impl<T, U> Into<U> for T
where U: From<T>,

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

impl<T, U> TryFrom<U> for T
where U: Into<T>,

type Error = Infallible

The type returned in the event of a conversion error.

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.