((a, b), (c, d)) printed as ((a, b), c, d)

Stream: new members

[lorã]

theres a option to block that? Why is that happening? i mean, i would understand if it was (a, b, c, d). I tried to use the explicity of parens, but without success. Theres my code with outputs:

set_option pp.parens true

instance : Monad List where
  pure := ([·])
  bind := (·.flatMap)

def singProds (xs : List α) : List (α × α) := do
  let a ← xs
  let b ← xs
  return (a, b)

#eval singProds $ singProds ([1, 2, 3])     --> [((1, 1), 1, 1), ..]
#eval ((singProds [(1, 1), (2, 2)])[0])     --> ((1, 1), 1, 1)
#eval ((singProds [(1, 1), (2, 2)])[0]).fst --> (1, 1)
#eval ((singProds [(1, 1), (2, 2)])[0]).snd --> (1, 1)

#eval [((1, 2), (3, 4))]       --> [((1, 2), 3, 4)]
#eval ((1, 2), 3, 4)           --> ((1, 2), 3, 4)
#eval (((1, 2), (3, 4)) : (Nat × Nat) × (Nat × Nat))
  --> ((1, 2), 3, 4)

[suhr]

Why is that happening?

example: (1, 2, 3, 4) = (1, (2, (3, 4))) := rfl

That's how n-tuples are encoded in Lean.

[Kyle Miller]

Similar to function arrows, × is right associative, so A × B × C is A × (B × C). That's then reflected in the tuple syntax.

It's possible to override this:

import Lean

@[app_unexpander Prod.mk] def unexpandProdMkSimple : Lean.PrettyPrinter.Unexpander
  | `($(_) $x $y)          => `(($x, $y))
  | _                      => throw ()

#check ((1, 2), 3, 4)
-- ((1, 2), (3, 4))

[suhr]

But if you override this, you will get (1, (2, (3, 4))) for (1, 2, 3, 4).

[Kyle Miller]

Yes of course, that's the point of it.