|
|
|
|
|
|
by blueblimp
557 days ago
|
|
|
This sort of convenient semi-arbitrary extension of a partial function is ubiquitous in Lean 4 mathlib, the most active mathematics formalization project today. It turns out that the most convenient way to do informal math and formal math differ in this aspect. |
|
|