Extract an Int value from an app-spine whose head is `Int.ofNat` or `Int.negSucc` applied to a Nat literal. Returns `None` for any other shape so the caller leaves the expression unreduced for delta+iota to handle. Callers typically pass a whnf'd expression so partially-applied constructors (e.g. `Int.ofNat` with a non-literal argument) will naturally be rejected here.
( e: &KExpr<M>, prims: &Primitives<M>, )
| 3006 | let proof = self.intern(KExpr::app(proof_const, args[0].clone())); |
| 3007 | let proof = self.intern(KExpr::app(proof, args[1].clone())); |
| 3008 | let proof = self.intern(KExpr::app(proof, refl_proof)); |
| 3009 | |
| 3010 | // Build: Decidable.isFalse prop proof |
| 3011 | let is_false = self.intern(KExpr::cnst( |
| 3012 | self.prims.decidable_is_false.clone(), |
| 3013 | Box::new([]), |
| 3014 | )); |
| 3015 | let r = self.intern(KExpr::app(is_false, prop)); |
| 3016 | self.intern(KExpr::app(r, proof)) |
| 3017 | } else { |
| 3018 | // decLe false: the proof requires `Bool.noConfusion.{0} False Bool.false Bool.true` |
| 3019 | // which needs a `False` primitive not yet registered. Fall through to |
| 3020 | // delta reduction which correctly unfolds Nat.decLe to its definition body. |
| 3021 | return Ok(None); |
| 3022 | }; |
| 3023 | |
| 3024 | let mut result = result_expr; |
| 3025 | for arg in args.iter().skip(2) { |
| 3026 | result = self.intern(KExpr::app(result, arg.clone())); |
| 3027 | } |
| 3028 | Ok(Some(result)) |
| 3029 | } |
| 3030 | |
| 3031 | fn try_normalize_int_decidable( |
| 3032 | &mut self, |
no test coverage detected