Post #1629262

2026-04-23 11:28 UTC

Another day, another rant about injectivity: https://proofassistants.stackexchange.com/questions/6533/why-does-lean4-use-intensional-type-theory-when-its-definitional-equality-is-und Am I an old broken record already?

Replies (0)

No replies.