Skip to main content

admit

Function admit 

Source
pub fn admit(
    k: &mut Kernel,
    ctx: &Context,
    block: &[Declaration],
) -> Result<(), String>
Expand description

Admits one declaration, or one mutual block of inductive families, into a kernel built by Kernel::logos over ctx: the core’s verdict on it.