Function mk_addr

crates/kernel/src/inductive.rs:4513–4515

(s: &str)

  ///   2. Result universe is Prop (level is zero)
  ///   3. Exactly one constructor with zero non-param fields
  fn compute_k_target(&mut self, ind_id: &KId<M>) -> Result<bool, TcError<M>> {
    let (ind_params, ind_indices, ctors, block, ty) =
      match self.try_get_const(ind_id)? {
        Some(KConst::Indc { params, indices, ctors, block, ty, .. }) => {
          (params, indices, ctors.clone(), block.clone(), ty.clone())
        },