MonadLift Id m instance

Stream: lean4

[Eric Wieser]

Is this a sensible instance?

instance [Pure m] : MonadLift Id m where
  monadLift f := pure <| Id.run f

If so, does it belong in core? Std? Mathlib?

[Eric Wieser]

(cc @Scott Morrison, as this was in one of your PRs and I found I needed it in my refactor too)

[Scott Morrison]

I would put this in Std.