def Prod.mapAllM {M : Type (max u_1 u_2) → Type u_3} {α : Type u_4} {β : Type (max u_1 u_2)} [Monad M] (f : α → M β) : α × α → M (β × β)

Apply f to all elements of a tuple. All elements of the tuple must have the same type α.

Equations

• Prod.mapAllM f (x_1, y) = do let __do_lift ← f x_1 let __do_lift_1 ← f y pure (__do_lift, __do_lift_1)