Method validate_expr_well_scoped

crates/kernel/src/check.rs:500–576

(
    &mut self,
    root: &KExpr<M>,
    root_depth: u64,
    lvl_bound: usize,
    mut timing: Option<&mut ValidationTiming>,
  )

  ) -> 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,
    block: &KId<M>,
    expected: CheckBlockKind,
  ) -> Result<Option<KId<M>>, TcError<M>> {
    let Some(members) = self.try_get_block(block)? else {
      return Ok(None);
    };
    match self.classify_block(&members) {
      Ok(kind) if kind == expected => Ok(Some(block.clone())),
      Ok(_) | Err(_) => Ok(None),
    }
  }

  fn classify_block(
    &mut self,
    members: &[KId<M>],
  ) -> Result<CheckBlockKind, TcError<M>> {
    if members.is_empty() {
      return Err(TcError::Other("empty check block".into()));
    }

    let mut saw_defn = false;
    let mut saw_recr = false;
    let mut saw_inductive_like = false;
    for member in members {
      match self.get_const(member)? {
        KConst::Defn { .. } => saw_defn = true,
        KConst::Recr { .. } => saw_recr = true,
        KConst::Indc { .. } | KConst::Ctor { .. } => {
          saw_inductive_like = true;
        },
        KConst::Axio { .. } | KConst::Quot { .. } => {
          return Err(TcError::Other(format!(