Zulip Chat Archive

Stream: maths

Topic: pythagorean triples


view this post on Zulip Paul van Wamelen (Jun 27 2020 at 19:05):

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
?

view this post on Zulip Bhavik Mehta (Jun 27 2020 at 19:05):

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

view this post on Zulip Scott Morrison (Jun 28 2020 at 00:09):

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.


Last updated: May 14 2021 at 19:21 UTC