pub fn candidate_block(
ctx: &Context,
levels: Option<&[String]>,
block: &[MutualInductive],
) -> Vec<Declaration>Expand description
The block of inductive families a door of ctx puts to the core. Each arity is stored as
ctx stores it, and each member takes the stated telescope or its stored arity’s level
variables. A constructor’s bare reference to a member stands at that member’s telescope, and
one to anything else at the level ctx gives it.