伊莎貝爾：梅蒂斯：證明狀態包含通用排序{}

Question

梅蒂斯給我的警告：

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

這是什麼意思的警告？ 這是否表明metis證據比沒有警告的「不健康」？

Answer 1

這個證明絕對是合理的。我記得，這條消息對於開發者來說主要是有價值的，因爲它有助於診斷metis調用失敗的原因。正常HOL目標不包含空類別。

我的猜測是這個警告已經過時了。