In what intensional type theories can absurdity be m...
推文的連結找到 Agda 把 ＿|＿ 換成 proof irrelevant 的, 然後終於又找到可以不把 == pattern match 成 refl 卻又把不相等的 constructor 刪掉的功能的 issue 了..
[ fix #3526 ] Remove trivially impossible clauses fr...
但是這個跟 proof irrelevant == 結合起來到底在型別系統裡面語義是什麼啊
