|
|
|
|
|
|
by IshKebab
72 days ago
|
|
|
> Lean can deduce proofs implicitly as well. Sure, but you still have to explicitly ask it to. > What is a standard subtraction over natural numbers at all? If you need something that is always defined then you have to use a non-standard subtraction (i.e. saturating subtraction). In other words the `-` operator should not work for Nat. It should require you to use `-_`. |
|
|