(&self, e: &KExpr<M>)
| 2608 | step: &KExpr<M>, |
| 2609 | ) -> Result<bool, TcError<M>> { |
| 2610 | let step = self.whnf(step)?; |
| 2611 | let ExprData::Lam(_, _, _, body, _) = step.data() else { |
| 2612 | return Ok(false); |
| 2613 | }; |
| 2614 | let ExprData::Lam(_, _, _, body, _) = body.data() else { |
| 2615 | return Ok(false); |
| 2616 | }; |
| 2617 | |
| 2618 | let (head, args) = collect_app_spine(body); |
| 2619 | let ExprData::Const(id, _, _) = head.data() else { |
| 2620 | return Ok(false); |
| 2621 | }; |
| 2622 | if id.addr != self.prims.nat_succ.addr || args.len() != 1 { |
| 2623 | return Ok(false); |
| 2624 | } |
| 2625 | Ok(matches!(args[0].data(), ExprData::Var(0, _, _))) |
| 2626 | } |
| 2627 | |
| 2628 | fn nat_expr_from_value(&mut self, n: Nat) -> KExpr<M> { |
| 2629 | let blob_addr = Address::hash(&n.to_le_bytes()); |
| 2630 | KExpr::nat(n, blob_addr) |
| 2631 | } |
| 2632 | |
| 2633 | fn nat_succ_n(&mut self, mut e: KExpr<M>, n: u64) -> KExpr<M> { |
| 2634 | for _ in 0..n { |
no test coverage detected