akiaki的回答:
EXAMPLE里给出的有的代码实际在HOL4中没法复现。明天我试试你贴的这个对策里的例子 - satone 2020年6月26日 21:47
实验了,确实是!open Q可以看到:type tmquote = term quotation,quotation是用单点包裹的,我之前搞错了hhh - satone 2020年6月27日 12:48
返回顶部