Method nat_succ_n

crates/kernel/src/whnf.rs:1966–1973

(&mut self, mut e: KExpr<M>, n: u64)

    // Get the first constructor
    let ctor_id = match self.try_get_const(&ind_id)? {
      Some(KConst::Indc { ctors, .. }) if !ctors.is_empty() => ctors[0].clone(),
      _ => return Ok(None),
    };

    // Build nullary ctor application: Ctor.{levels} params...
    let ctor_us = match ty_head.data() {
      ExprData::Const(_, us, _) => us.clone(),
      _ => return Ok(None),
    };
    let mut ctor_app = self.intern(KExpr::cnst(ctor_id, ctor_us));
    for arg in ty_args.iter().take(recr.params) {