Method check_ctor_against_inductive_member

crates/kernel/src/inductive.rs:360–424

Validate a standalone constructor against its parent inductive. Runs the same A1–A4 checks that `check_inductive_member` runs per-ctor.

(
    &mut self,
    ctor_id: &KId<M>,
    induct_id: &KId<M>,
  )

        KConst::Indc {
          params, indices, lvls, block, is_unsafe, ty, ..
        } => (params, indices, lvls, block.clone(), is_unsafe, ty.clone()),
        _ => {
          return Err(TcError::Other(
            "check_ctor: parent inductive not found".into(),
          ));
        },
      };

    let block_inds = self.discover_block_inductives(&ind_block)?;
    let block_addrs: Vec<Address> =
      block_inds.iter().map(|id| id.addr.clone()).collect();

    let ind_level = self.get_result_sort_level(
      &ind_ty,
      u64_to_usize(ind_params + ind_indices)?,
    )?;

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

    // A3: Strict positivity. Match Lean: unsafe inductives bypass this check.
    if !ind_is_unsafe {
      self.check_positivity(
        &ctor_ty,
        u64_to_usize(ind_params)?,
        &block_addrs,
      )?;
    }

    // A4: Universe constraints
    self.check_field_universes(
      &ctor_ty,
      u64_to_usize(ind_params)?,
      &ind_level,
    )?;

    // A2: Constructor return type
    self.check_ctor_return_type(
      &ctor_ty,
      u64_to_usize(ind_params)?,
      u64_to_usize(ind_indices)?,
      ctor_fields,
      &induct_id.addr,
      ind_lvls,
      &block_addrs,
    )?;

    Ok(())
  }

  /// Discover all inductives in a mutual block.
  fn discover_block_inductives(
    &mut self,
    block_id: &KId<M>,
  ) -> Result<Vec<KId<M>>, TcError<M>> {
    let Some(members) = self.try_get_block(block_id)? else {
      return Ok(vec![]);
    };