Lean4
/-- Given `e = f a₁ a₂ ... aₙ`, returns `k f #[a₁, ..., aₙ]` where `f` can be bundled morphism. -/
partial def withApp {α} (e : Expr) (k : Expr → Array Arg → MetaM α) : MetaM α :=
go e #[]
where/-- -/
go : Expr → Array Arg → MetaM α
| .mdata _ b, as => go b as
| .app (.app c f) x, as => do
if ← isCoeFun c then
go f (as.push { coe := c, expr := x })
else
go (.app c f) (as.push { expr := x })
| .app (.proj n i f) x, as => do
-- convert proj back to function application
let env ← getEnv
let info := getStructureInfo? env n |>.get!
let projFn := getProjFnForField? env n (info.fieldNames[i]!) |>.get!
let .app c f ← mkAppM projFn #[f] |
panic! "bug in Mor.withApp"
go (.app (.app c f) x) as
| .app f a, as => go f (as.push { expr := a })
| f, as => k f as.reverse
