Method discover_block_inductives

crates/kernel/src/inductive.rs:427–441

Discover all inductives in a mutual block.

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

    // Validate each constructor
    for (expected_cidx, ctor_id) in ctors.iter().enumerate() {
      let ind_params = u64_to_usize(params)?;
      let (ctor_ty, ctor_fields) = self.check_ctor_metadata_against_parent(
        ctor_id,
        id,
        expected_cidx,
        ind_params,
        lvls,
        is_unsafe,
      )?;

      // A1: Parameter domain agreement
      self.check_param_agreement(&ty, &ctor_ty, ind_params)?;

      // A3: Strict positivity. Lean skips positivity for unsafe inductives;
      // those declarations are admitted only as unsafe constants.
      if !is_unsafe {
        self.check_positivity(&ctor_ty, ind_params, &block_addrs)?;