Function extract_nat_lit

crates/kernel/src/whnf.rs:2851–2862

Extract a nat value from a literal or `Nat.zero` constructor. Matches both `Nat(n)` literals and the `Nat.zero` constructor constant, mirroring C++ `is_nat_lit_ext` and lean4lean `rawNatLitExt?`. After iota reduction, `Nat.zero` can appear as `Const(Nat.zero, [])` which must be recognized for native Nat operations to fire.

(
  e: &'a KExpr<M>,
  prims: &Primitives<M>,
)

        )
      },
      _ => false,
    }
  }

  /// 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 : Prop) → (p → False) → Decidable p`
  /// so the proposition `p` must be supplied as the first argument.