inline extract value from monad

Stream: lean4

[Locria Cyber]

I currently have

def fromLines : List String -> Option (List Nat)
| [] => some []
| (x :: xs) => do
  let x' <- x.data.mapA charToNat
  let xs' <- fromLines xs
  x' ++ xs'

Is there a shorter way to write this? e.g. (x' ++ extract_keyword! (fromLines xs))

[Henrik Böving]

You can do stuff like

let x := (<-a) + (<-b)

The () around the "inline" arrows are important