Method try_reduce_nat_predicate

crates/kernel/src/whnf.rs:2031–2054

(
    &mut self,
    addr: &Address,
    args: &[KExpr<M>],
  )

    let (head, args) = collect_app_spine(wval);

    if let Some(result) =
      self.try_reduce_fin_val_decidable_rec(id, field, &head, &args)
    {
      self.dump_proj_trace(id, field, wval, None, Some(&result));
      return Ok(Some(result));
    }

    let ctor_id = match head.data() {
      ExprData::Const(id, _, _) => id,
      _ => {
        self.dump_proj_trace(id, field, wval, None, None);
        return Ok(None);
      },
    };

    let ctor_params = match self.try_get_const(ctor_id)? {
      Some(KConst::Ctor { params, .. }) => match usize::try_from(params) {
        Ok(params) => params,
        Err(_) => return Ok(None),
      },
      _ => {
        self.dump_proj_trace(id, field, wval, None, None);
        return Ok(None);
      },
    };