如何初始化空提示數據庫

Question

我有幾個證據遵循相同的結構。其中第一個可以用trivial完成，其他所有用auto with foo_db完成，其中foo_db是在第一個證明完成後填充提示的提示數據庫。我想寫一個使用auto with foo_db來解決所有這些證明的Ltac程序。但是，當運行該Ltac解決我的第一個證明foo_db尚不存在，所以科克抱怨：Error: No such Hint database: foo_db.。有沒有辦法初始化一個空的提示數據庫？

Answer 1

是的，有一個命令Create HintDb，正是你想要的。

Create HintDb foo_db. 

Goal True. 
    auto with foo_db nocore. (* no hints *) 
    exact I. 
Qed. 

出於演示的目的（避免解決的目標），我還添加了僞DB nocore避免使用標準庫的提示。您可能只想做auto with foo_db，以解決trivial本來可以解決的所有目標。