Flatten nested ``Expr.app(f, x)`` into ``(head, [arg0, arg1, ...])``.
(expr: LeanInductiveValue)
| 56 | |
| 57 | |
| 58 | def uncurry_app(expr: LeanInductiveValue) -> tuple[LeanInductiveValue, list[LeanInductiveValue]]: |
| 59 | """Flatten nested ``Expr.app(f, x)`` into ``(head, [arg0, arg1, ...])``.""" |
| 60 | args: list[LeanInductiveValue] = [] |
| 61 | cur = expr |
| 62 | while cur.ctor == "app": |
| 63 | args.append(cur._1) # arg |
| 64 | cur = cur._0 # fn |
| 65 | args.reverse() |
| 66 | return cur, args |
| 67 | |
| 68 | |
| 69 | # --------------------------------------------------------------------------- |