Function env_with_id

crates/kernel/src/whnf.rs:3096–3151

Build a minimal env with a single definition: `id := λ x. x : Sort 0 → Sort 0`

()

      (3usize, 4usize)
    } else {
      return Ok(None);
    };

    let major_whnf = self.whnf(&args[major_idx])?;
    let (mk_head, mk_args) = collect_app_spine(&major_whnf);
    let mk_addr = match mk_head.data() {
      ExprData::Const(id, _, _) => &id.addr,
      _ => return Ok(None),
    };
    if *mk_addr != self.prims.quot_ctor.addr {
      return Ok(None);
    }

    // Quot.mk has exactly 3 args: (α, r, a). Value is the last.
    if mk_args.len() != 3 {
      return Ok(None);
    }
    let quot_val = mk_args[2].clone();

    let mut result = self.intern(KExpr::app(args[f_idx].clone(), quot_val));
    for arg in args.iter().skip(major_idx + 1) {
      result = self.intern(KExpr::app(result, arg.clone()));
    }
    Ok(Some(result))
  }

  // -----------------------------------------------------------------------
  // BitVec reduction
  // -----------------------------------------------------------------------

  /// Reduce the small BitVec fragment that is definitionally Nat-backed:
  /// - `BitVec.toNat (BitVec.ofNat w n)` reduces to `n % 2^w`
  /// - `BitVec.ult w x y` reduces by evaluating `x.toNat < y.toNat`
  /// - `decide (x < y)` for BitVec reduces through the same comparison
  fn try_reduce_bitvec(
    &mut self,
    e: &KExpr<M>,
  ) -> Result<Option<KExpr<M>>, TcError<M>> {
    let (head, args) = collect_app_spine(e);
    let ExprData::Const(id, _, _) = head.data() else {
      return Ok(None);
    };

    if id.addr == self.prims.bit_vec_to_nat.addr && args.len() >= 2 {
      if let Some(result) = self.try_reduce_bitvec_to_nat(&args[1])? {
        return Ok(Some(self.finish_app_result(result, &args, 2)));
      }
      return Ok(None);
    }

    if id.addr == self.prims.bit_vec_ult.addr && args.len() >= 3 {
      if let Some(result) =
        self.try_reduce_bitvec_ult(&args[0], &args[1], &args[2])?
      {
        return Ok(Some(self.finish_app_result(result, &args, 3)));
      }
      return Ok(None);
    }