This is mostly designed for the Lean backend but could also apply to other. We need to insert nodes (resugaring?) to indicate that a sub-expression needs to be done inside the Result monad (inserting pure). Conversely, we need to insert nodes to "lift out of the monad", using <- in Lean.
Right now, both nodes are inserted during printing in a non-principled manner.
This is mostly designed for the Lean backend but could also apply to other. We need to insert nodes (resugaring?) to indicate that a sub-expression needs to be done inside the
Resultmonad (insertingpure). Conversely, we need to insert nodes to "lift out of the monad", using<-in Lean.Right now, both nodes are inserted during printing in a non-principled manner.