Method validate_const_well_scoped_timed

crates/kernel/src/check.rs:435–484

(
    &mut self,
    c: &KConst<M>,
    mut timing: Option<&mut ValidationTiming>,
  )

        self.check_recursor_member(id)?;
        Ok(())
      },

      KConst::Indc { ty, .. } => {
        let t = self.infer(ty)?;
        self.ensure_sort(&t)?;
        self.check_inductive_member(id)?;
        Ok(())
      },

      KConst::Ctor { ty, induct, .. } => {
        let t = self.infer(ty)?;
        self.ensure_sort(&t)?;
        // Validate against the parent inductive (A1–A4 checks).
        // This ensures standalone ctorInfo is rejected if it doesn't
        // match its declared inductive.
        let induct = induct.clone();
        self.check_ctor_against_inductive_member(id, &induct)?;
        Ok(())
      },
    }
  }

  fn coordinated_block_for(
    &mut self,
    c: &KConst<M>,
  ) -> Result<Option<KId<M>>, TcError<M>> {
    match c {
      KConst::Defn { block, .. } => {
        self.coordinated_block_if_kind(block, CheckBlockKind::Defn)
      },
      KConst::Indc { block, .. } => {
        self.coordinated_block_if_kind(block, CheckBlockKind::Inductive)
      },
      KConst::Ctor { induct, .. } => {
        let Some(parent) = self.try_get_const(induct)? else {
          return Ok(None);
        };
        match parent {
          KConst::Indc { block, .. } => {
            self.coordinated_block_if_kind(&block, CheckBlockKind::Inductive)
          },
          _ => Ok(None),
        }
      },
      KConst::Recr { block, .. } => {
        self.coordinated_block_if_kind(block, CheckBlockKind::Recursor)
      },
      KConst::Axio { .. } | KConst::Quot { .. } => Ok(None),
    }
  }

  fn coordinated_block_if_kind(
    &mut self,