coq検索とバリアントで既存のファクトを検索する


構文

  • Search qualid. (* Coq 8.4以降のバージョンでは*)
  • SearchAbout qualid. (*非推奨の同義語*)

パラメーター

パラメータ 説明
qualid 検索する識別子またはパターン。それは記法を含むことができる

備考

Coq 8.4以前では、 Searchは現在のSearchHead意味を持っていました。文の終わ​​りにパターンが一致するファクトのみを検索します。

検索とバリアントで既存のファクトを検索する 関連する例