Confusion with Pos.asNat traversing application

Stream: metaprogramming / tactics

[Tomás Díaz]

Hi, I'm trying to traverse an application (Expr) and apply a cast operator on each argument but I'm a bit confused with some results. This is in Lean 4 (not sure if this stream is for Lean 3 or 4).

I was trying Expr.traverseAppWithPos to traverse the application, but without applying the function to the first position and so I thought I could simply do something like the following:

def foobar (pos : SubExpr.Pos) (e : Expr) : TermElabM Expr :=
  match SubExpr.Pos.asNat pos with
  | 0 => -- ignore
  | _ => -- do something else

But somehow when applying Pos.asNat I'm getting indices like 4, 5, 16, etc. And I'm a bit confused why?
For instance, using dbg_trace I get:

dbg_trace pos -- /0
dbg_trace (Pos.asNat pos) -- 4

In any case, I'll probably just extract the args with getAppArgs and map it, but I was confused with those results.
(If there are better ways lmk, please :) )