Method coordinated_block_for

crates/kernel/src/check.rs:257–284

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

  }

  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,