Termination in Computed Fields

Stream: lean4

[Andrés Goens]

Is there a way to show termination for a computed_field function? A simple example for the depth of a tree:

inductive NatTree where
    | leaf (val : Nat) : NatTree
    | parent (val : Nat) (children : List NatTree) : NatTree
with
    @[computed_field] depth : NatTree → Nat
      | .leaf _ => 1
      | .parent _ []  => 1
      -- | .parent a (ch::chs) => 1 + max (depth ch) (depth $ NatTree.parent a chs)
      -- computed field NatTree.depth does not reduce for constructor NatTree.parent
      | .parent a ch@(_::_) => 1 + (ch.map depth).maximum?.get!
        decreasing_by sorry
      --^ expected command

The first option would go through with structural recursion but won't work (I imagine that's the same as the TODO for patterns like .app (.app a b) c), whereas the second option won't go through without termination and it seems I can't add some termination to that.