coq Searching for an existing fact with Search and variants

Help us to keep this website almost Ad Free! It takes only 10 seconds of your time:
> Step 1: Go view our video on YouTube: EF Core Bulk Extensions
> Step 2: And Like the video. BONUS: You can also share it!

Syntax

  • Search qualid. (* for Coq 8.4 and newer versions *)
  • SearchAbout qualid. (* deprecated synonym. *)

Parameters

ParameterDescription
qualidThe 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.



Got any coq Question?