isabelle - Isabelle：Metis：证明状态包含通用排序 {}

Question

梅蒂斯给了我警告：

Metis: Proof state contains the universal sort {} 
("HOL/Tools/Metis/metis_tactic.ML")

这个警告是什么意思？这是否表明metis证明比没有警告时“不那么健全”？

Answer 1

证据肯定是正确的。我记得，这条消息主要对开发人员有价值，用于帮助诊断 metis 调用失败的原因。正常的 HOL 目标不包含空排序。

我的猜测是这个警告已经过时了。