Native Nat.decLe/decEq/decLt reduction. Intercepts `Nat.decLe n m`, `Nat.decEq n m`, `Nat.decLt n m` when both arguments are Nat literals. Computes the boolean result natively and constructs the appropriate `Decidable.isTrue prop proof` or `Decidable.isFalse prop proof`. Constructors in the kernel are fully explicit: `Decidable.isTrue : (p : Prop) → p → Decidable p` `Decidable.isFalse : (p : Pr
(
&mut self,
e: &KExpr<M>,
)
| 2200 | return None; |
| 2201 | }; |
| 2202 | let idx = usize::try_from(*idx).ok()?; |
| 2203 | if idx >= arity { |
| 2204 | return None; |
| 2205 | } |
| 2206 | let struct_arg_idx = arity - 1 - idx; |
| 2207 | return Some((arity, struct_id.clone(), *field, struct_arg_idx)); |
| 2208 | }, |
| 2209 | _ => return None, |
| 2210 | } |
| 2211 | } |
| 2212 | } |
| 2213 | |
| 2214 | // ----------------------------------------------------------------------- |
| 2215 | // Helpers |
| 2216 | // ----------------------------------------------------------------------- |
| 2217 | |
| 2218 | /// Get the major premise's inductive KId from a recursor type. |
| 2219 | /// |
| 2220 | /// Strategy: peel `skip` foralls per Lean's stored `params + motives + |
| 2221 | /// minors + indices` count, then expect the next forall's domain to |
| 2222 | /// have an inductive `Const` head. For well-formed Lean recursors this |
| 2223 | /// lands exactly on the major premise. |
| 2224 | /// |
| 2225 | /// Resilience: if the strict `skip` position's domain head is not an |
| 2226 | /// inductive `Const`, peel up to `MAX_EXTRA_FORALLS` additional foralls |
| 2227 | /// scanning for the first one whose domain head IS an inductive |
| 2228 | /// `KConst::Indc`. This handles recursor shapes where Lean's stored |
| 2229 | /// counts don't align with the kernel's view of the forall structure |
| 2230 | /// after WHNF (e.g., nested-inductive recursors that carry extra |
| 2231 | /// instance/motive binders not captured by `num_params/num_motives/...`). |
| 2232 | /// |
| 2233 | /// We specifically require the head to be an **inductive** constant, not |
| 2234 | /// any Const: minor premises of recursors like `Nat.rec`'s `succ` case |
| 2235 | /// have a forall `(n : Nat)` where `Nat` is a Const inductive, but |
| 2236 | /// those are consumed by the initial `skip` pass. The scan only ever |
| 2237 | /// fires when `skip` under-counts; in that case the first Const |
| 2238 | /// inductive encountered is structurally the major. |
| 2239 | pub fn get_major_inductive_id( |
| 2240 | &mut self, |
| 2241 | rec_ty: &KExpr<M>, |
| 2242 | skip: u64, |
| 2243 | ) -> Result<KId<M>, TcError<M>> { |
| 2244 | const MAX_EXTRA_FORALLS: u64 = 8; |
| 2245 | let saved = self.save_depth(); |
| 2246 | let result = (|| -> Result<KId<M>, TcError<M>> { |
| 2247 | let mut ty = rec_ty.clone(); |
| 2248 | for _ in 0..skip { |
| 2249 | let w = self.whnf(&ty)?; |
| 2250 | match w.data() { |
| 2251 | ExprData::All(_, _, dom, body, _) => { |
| 2252 | // Keep the peeled binder in scope. The body is open, and must not |
| 2253 | // resolve one of its Vars through an unrelated caller frame. |
| 2254 | self.push_local(dom.clone()); |
| 2255 | ty = body.clone(); |
| 2256 | }, |
| 2257 | _ => { |
| 2258 | return Err(TcError::Other( |
| 2259 | "get_major_inductive_id: not enough foralls".into(), |
no test coverage detected