variable vs constant

Stream: new members

[Kevin Buzzard]

The answer is that constant (A : B) adds a new declaration A to the system with no definition, but variable just inserts (A : B) as an assumption in all the theorems and definitions you make which mention A. But what you really need to know is: if in doubt, use variable (and definitely read Patrick's link!)

[Matúš Behun]

Thanks, I've actually read what Patrick posted but difference seemed too subtle to me. I am trying to to formulate how I would explain what's the difference between those two and way to explain it for me is that they have different purpose.

[Scott Morrison]

The main difference is that you shouldn't use constant, and you should use variable. :-)

[Matúš Behun]

and what about axiom is that alias for constant?

[Scott Morrison]

As far as I know. Both are useless if you're doing "normal maths", perhaps outside of writing unit tests for tactics.

[Matúš Behun]

okay, I will move on