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.

[James Gallicchio]

did this end up in std now batteries? I haven't searched very hard but #synth isn't coming up with anything

[Kim Morrison]

Probably not!