| 3186 | self.prims.bool_false.clone() |
| 3187 | }; |
| 3188 | let result = self.intern(KExpr::cnst(result_id, Box::new([]))); |
| 3189 | return Ok(Some(result)); |
| 3190 | } |
| 3191 | } |
| 3192 | |
| 3193 | // `BitVec.ult x y` is definitionally `decide (x.toNat < y.toNat)`. |
| 3194 | // Kernel Nat LT reduces through `Nat.ble (Nat.succ x.toNat) y.toNat`. |
| 3195 | let lhs_succ = self.nat_succ_n(lhs_nat, 1); |
| 3196 | let ble = |
| 3197 | self.intern(KExpr::cnst(self.prims.nat_ble.clone(), Box::new([]))); |
| 3198 | let cmp_lhs = self.intern(KExpr::app(ble, lhs_succ)); |
| 3199 | let cmp = self.intern(KExpr::app(cmp_lhs, rhs_nat)); |
| 3200 | let result = self.whnf(&cmp)?; |
| 3201 | if self.bool_lit_value(&result).is_some() { |
| 3202 | Ok(Some(result)) |