Function whnf_beta_simple

crates/kernel/src/whnf.rs:3177–3185

()

      if rhs_val.0 == num_bigint::BigUint::ZERO {
        let result =
          self.intern(KExpr::cnst(self.prims.bool_false.clone(), Box::new([])));
        return Ok(Some(result));
      }

      let lhs_nat_whnf = self.whnf(&lhs_nat)?;
      if let Some(lhs_val) = extract_nat_value(&lhs_nat_whnf, &self.prims) {
        let result_id = if lhs_val.0 < rhs_val.0 {
          self.prims.bool_true.clone()
        } else {
          self.prims.bool_false.clone()
        };
        let result = self.intern(KExpr::cnst(result_id, Box::new([])));