Method check_inductive

crates/kernel/src/inductive.rs:71–95

Validate an inductive block. Pure inductive blocks are coordinated through `KEnv`; legacy mixed source blocks fall back to the member check to avoid caching a partial result under a mixed block id.

(&mut self, id: &KId<M>)

/// A member of the "flat" mutual block used for recursor generation.
/// For non-nested inductives, this is just the original inductive.
/// For nested occurrences (e.g., `Array Syntax` in Syntax's ctor fields),
/// an auxiliary entry is created mirroring the external inductive's structure.
#[derive(Clone)]
pub struct FlatBlockMember<M: KernelMode> {
  /// For original: the inductive's KId. For auxiliary: the external inductive's KId.
  pub id: KId<M>,
  /// True if this is an auxiliary member created for a nested occurrence.
  pub is_aux: bool,
  /// Specialized param values for this member.
  /// For original: Var refs to the recursor's shared params.
  /// For auxiliary: the concrete specialized exprs (e.g., `[Syntax]` for `Array Syntax`).
  /// These are in terms of the recursor's param binders (depth = n_rec_params).
  pub spec_params: Vec<KExpr<M>>,
  /// Number of params this member's inductive has (may differ from shared for nested).
  pub own_params: u64,
  /// Number of indices.
  pub n_indices: u64,
  /// Constructor ids (from env).
  pub ctors: Vec<KId<M>>,
  /// Universe param count.
  pub lvls: u64,
  /// Universe args for internal processing (abstract shifted params).
  /// Used for ctor type instantiation and nesting detection.
  pub ind_us: Box<[KUniv<M>]>,
  /// Universe args from the actual nested occurrence (concrete).
  /// For original members: same as ind_us.
  /// For auxiliaries: the concrete args from the ctor field (e.g., [Succ(Zero)]).
  /// Used for the final output type (motives, major, ctor apps).