|
|
|
|
|
|
by momentoftop
1163 days ago
|
|
|
Ah, thanks for the link. I suggested the reason that Isabelle/HOL does this is because it requires total functions and you don't have a convenient way to do refinement types. But that's not an adequate explanation, because Lean does allow such refinements, but it still turns out to be inconvenient for division. I will note that setting a - b = 0 for a <= b is pretty standard, and is often called "partial subtraction." |
|
|