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:

  1. open import Agda.Builtin.Char
  2. open import Agda.Builtin.Char.Properties
  3. open import Agda.Builtin.String
  4. 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