Negtive numbers

Stream: lean4

[Min-Hsien Weng]

I am new to Lean 4, and I am trying to learn how to use it to evaluate mathematical expressions. I recently tried to evaluate the expression 0 - 1 = 0, but to my surprise, the result was true. I am wondering if there is something that I am doing wrong, or if this is a known issue in Lean 4. I have attached my code below. Thank you.
image.png

[Henrik Böving]

This is not an issue this is mostly just how it was decided to define this. THe alternative would be to force you to proof that whenever you do Nat.sub n m m < n. But that just makes many things tedious since the majority of uses of Nat.sub already implicitly do stuff like this. Providing a garbage value instead of limiting the domain of a function is a very common thing that other ITPs like Coq also do.

[Jannis Limperg]

Additional context: numeric literals, like 0 and 1, are interpreted as natural numbers unless the context makes it clear that they should be integers (or complex numbers etc.). So your statements means (0 : Nat) - (1 : Nat) = (0 : Nat).

[Kyle Miller]

and (0 : Int) - (1 : Int) = (0 : Int) is happily false

[Min-Hsien Weng]

It was my bad! I forgot to declare the type.
By supplying the type information, the evaluation result is correct. Awesome :tada:
image.png
Thanks @Henrik Böving @Kyle Miller @Jannis Limperg