coq Searching for an existing fact with Search and variants
Syntax
Search qualid.(* for Coq 8.4 and newer versions *)SearchAbout qualid.(* deprecated synonym. *)
Parameters
| Parameter | Description |
|---|---|
qualid | The identifier or pattern to search for. It can involve notations |
Remarks
Before Coq 8.4, Search had the meaning of the current SearchHead: only search for facts where the pattern matches in the conclusion of the statement.
