Изабель: Метис: состояние доказательства содержит универсальную сортировку {}

Метис предупреждает меня:

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

Что означает это предупреждение? Означает ли это, что метис-доказательство «менее надежно», чем без предупреждения?


isabelle
person mrsteve    schedule 27.11.2013    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Доказательства определенно веские. Насколько я помню, это сообщение в основном представляет ценность для разработчиков, поскольку помогает диагностировать, почему вызов metis не работает. Обычные цели HOL не содержат пустых сортировок.

Я предполагаю, что это предупреждение устарело.

person Lawrence Paulson    schedule 26.12.2013