Is Prod associative?

Stream: lean4

[Tim Hunter]

I noticed that (Int × Int) × (Int × Int) evaluates to the same time as (Int × Int) × Int × Int. Can see some good mathematical reasons for doing that, but this leads to the following rather intuitive behavior:

let l3 : List (Prod (Prod Int Int) (Prod Int Int)) := [((1,2), (3,4))]
-- Expected
l3.map (fun ((x1, x2), (x3, x4)) => 1)
-- Not expected
l3.map (fun ((x1, x2), x3, x4) => 1)