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