my stance on definitional equality is my stance on genders, either there should be no defeq at all, or anything you want can be defeq
@Vierkantor defeq? what does that mean
@LunaDragofelis definitional equality, defeq for short, is a concept in type theory. basically, you have propositional equality that you have to supply a proof for, and definitional equality that follows from the rules of the system and any definitions that you make.
for example in Lean, if a is a natural number, "a + 0 = a" is a definitional equality but "0 + a = a" does not hold definitionally, only propositionally.
@LunaDragofelis the reason you would want definitional equality is that you can use it automatically. so if you prove something about all numbers smaller than `a + b`, and want to apply it to the numbers smaller than `a`, then you are immediately done by setting `b = 0`.
but the drawback is that it does not work if instead you want to apply it to the numbers smaller than `b` by setting `a = 0`
@Vierkantor I don't understand any of this…
@LunaDragofelis in the programming metaphor, the two options I'm advocating are either to just remove the "crash on wrong definition" feature completely, or allow you to specify that more definitions are right and not provoke a crash. that's the gist of it.
@Vierkantor I see. Because my behavior in school was too bad, I was put in special education (Förderschule) and we never got above basic math there
if I had it in school I'd likely understand that stuff and I'm mad about it
@LunaDragofelis @Vierkantor I majored in mathematics (with specialization in computational logic!) and I also have difficulties understanding it!
@LunaDragofelis sorry, I always find it hard to estimate at which level to start!
let's try from a programming POV: imagine what a pain it would be if any part of your program would be allowed to depend on the exact way you write code in any other part. not just the return values, but also e.g. the order in which you put two if statements, and crash if it's wrong.
well, it turns out definitional equality in certain ("intensional") type theories does basically this.