use*_*970 1 logic proof agda
我想澄清一下agda中的双重否定.
即使
z?z : 0 ? 0 z?z = refl
我无法弄清楚如何证明:
¬¬z?z : (0 ? 0 ? ?) ? ? ¬¬z?z ?
这是长期的¬ (0 ? 0).也许我错过了一路上的agda成语.理想我想要一个最小参考标准库的解释.
¬ (0 ? 0)
asr*_*asr 6
您可以证明¬¬z?z通过
¬¬z?z
¬¬z?z : (0 ? 0 ? ?) ? ? ¬¬z?z h = h refl
归档时间：
12 年，1 月 前
查看次数：
249 次
最近记录：