Search Definitions in Scope
Since version 2.5.1 Agda supports the command Search About
that searches
the objects in scope, looking for definitions matching a set of constraints
given by the user.
Usage
The tool is invoked by choosing Search About
in the goal menu or pressing
C-c C-z
. It opens a prompt and users can then input a list of space-separated
identifiers and string literals. The search returns the definitions in scope whose
type contains all of the mentioned identifiers and whose name contains all of
the string literals as substrings.
For instance, in the following module:
open import Agda.Builtin.Char
open import Agda.Builtin.Char.Properties
open import Agda.Builtin.String
open import Agda.Builtin.String.Properties
running Search About
on Char String
returns:
- Definitions about Char, String
- primShowChar
: Char → String
- primStringFromList
: Agda.Builtin.List.List Char → String
- primStringToList
: String → Agda.Builtin.List.List Char
- primStringToListInjective
- : (a bString) →
primStringToList a Agda.Builtin.Equality.≡ primStringToList b → a Agda.Builtin.Equality.≡ b
and running Search About
on String "Injective"
returns:
- Definitions about String, “Injective”
- primStringToListInjective
- : (a bString) →
primStringToList a Agda.Builtin.Equality.≡ primStringToList b → a Agda.Builtin.Equality.≡ b