An example

Stream: new members

[Alex Zhang]

I don't understand what the following example means. Could anyone please give an explanation?
example : Σ x y : ℤ, (ℤ × ℤ) × ℤ := by use [1, 2, 3, 4, 5]

[Mario Carneiro]

what needs explaining exactly?

[Alex Zhang]

I don't understand the sigma notation here

[Mario Carneiro]

The type involves a few ways to tuple numbers together and basically says "five ints", and the proof is saying "(1,2,3,4,5) is five ints"

[Mario Carneiro]

Sigma is a dependent tuple type: an element of Σ x : A, B x is a pair (a, b) where a : A and b : B a

[Mario Carneiro]

In this case, it's not actually dependent, so it's equivalent to using ×