def Prod.mapM {m : Type → Type} {α β δ γ : Type} [Monad m] (f : α → m β) (g : δ → m γ) (x : α × δ) : m (β × γ)

Equations

• Prod.mapM f g x = Prod.mk <$> f x.fst <*> g x.snd

@[reducible, inline]

abbrev Prod.thd {α β γ : Type} (x : α × β × γ) : γ

Equations

• x.thd = x.snd.snd

def Prod.map₃ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} {ζ : Type u_6} (f : α → δ) (g : β → ε) (h : γ → ζ) : α × β × γ → δ × ε × ζ

Exposed: Core/GuardedPlusCal/Semantics/Lemmas.lean reasons about map₃ applied to a literal triple, which needs the body to reduce.

Equations

• Prod.map₃ f g h (x_1, y, z) = (f x_1, g y, h z)

def Prod.traverse₃ {α β γ δ ε ζ : Type} {F : Type → Type} [Applicative F] (f : α → F δ) (g : β → F ε) (h : γ → F ζ) : α × β × γ → F (δ × ε × ζ)

Equations

• Prod.traverse₃ f g h (x_1, y, z) = (fun (x1 : δ) (x2 : ε) (x3 : ζ) => (x1, x2, x3)) <$> f x_1 <*> g y <*> h z

def Prod.dup {α : Type u} (x : α) : α × α

Equations

• Prod.dup x = (x, x)

@[reducible, inline]

abbrev Prod.hasDecEq {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] : DecidableEq (α × β)

Equations

• Prod.hasDecEq = inferInstance

theorem MProd.ext {α β : Type u_1} {x y : MProd α β} : x.fst = y.fst → x.snd = y.snd → x = y

theorem MProd.ext_iff {α β : Type u_1} {x y : MProd α β} : x = y ↔ x.fst = y.fst ∧ x.snd = y.snd