Why does Lean4 use intensional Type Theory when its definitional equality is undecidable anyways? – proofassistants.stackexchange.com

Hopefully this is not a too silly question, but I'm trying to understand the design choices made by the developers of proof assistants and how these choices help (or impede) human mathematicians to ...