The issue with special definitions is you can use them to say anything you want, turning regular, common operations into weirdness.
What does it mean to take a factorial on the real numbers, or to add only on the even integers? In both cases, we're twisting what are generally accepted mechanics and domains into something else to get a funny result, like 1/0 = 0.
He gets to that point here:
" We can say that division’s domain is all the real numbers except zero. This is what we do in our day-to-day lives, and the way that Agda and Idris handle division. We can choose some value that isn’t a real number, such as “undefined” or infinity, and say x/0 = <whatever>. This is what some mathematicians do with the Riemann sphere. We could choose some real number, like 19, and say that x/0 = 19. This is what Isabelle, Lean and Coq do.
"
So, tiny change in definition --> big change in outcome.
*I'm an undergrad