pythagorean triples

Stream: maths

[Paul van Wamelen]

What is the difference between writing
def pythagorean_triple (x y z : ℤ) := x*x + y*y = z*z
and
def pythagorean_triple (x y z : ℤ) : Prop := x*x + y*y = z*z
?

[Bhavik Mehta]

Basically nothing, but it's good to have the explicit type there for readability

[Scott Morrison]

In particular, it makes it trivial to see, before passing the :=, that you are defining a predicate, rather than constructing some actual pythagorean triple based on a choice of x y z. It's not immediately clear just from the name.