Agda: Vector Membership in Stdlib? (And how to learn stdlib in general)

Question

I'm dealing with strings in Agda, and I've got a vector of them. I need to check if a given string occurs in a vector (as a part of checking if a variable is free or bound in an expression, in PL theory wprk I'm doing).

I'm still finding my way around the standard library, and I'm finding that I'm spending a lot of time looking for basic functions that would be in the standard library in other languages (Haskell, etc.). There's great resources for learning the language and its concepts, but not a lot that I've seen for applied programming in Agda, common libraries, etc.

Is there a membership function for Vectors in the standard library, or an easy one-liner to construct one, or do I need to write the function myself? (Obviously such a function would be parameterized over decidable equality for the element type)
How do you learn the standard library in Agda? Are there good guides/tutorials, or a hoogle-like tool?

gallais gallais · Accepted Answer · 2017-03-07T03:15:17

Is there a membership function for Vectors in the standard library, or an easy one-liner to construct one, or do I need to write the function myself?

Not that I know of. The right notions are there but not the search function AFAICT. And using the command I describe in the rest of the answer doesn't yield any result.

How do you learn the standard library in Agda? Are there good guides/tutorials, or a hoogle-like tool?

Inside emacs you can use C-c C-z to search the definitions in scope. You can use both identifiers (it'll select the definitions whose type mentions them) and string literals (it'll select the ones whose identifier contains that string).

As a consequence, one way to explore the library is to open import a lot of modules and use C-c C-z on carefully selected keywords. E.g. in the following module

module Explore where

open import Data.Nat
open import Data.Nat.Divisibility
open import Data.Nat.Properties
open import Data.Nat.Properties.Simple

the keystroke C-c C-z _*_ _+_ RET returns:

Definitions about _*_, _+_
  +-*-suc : (m n : ℕ) → m * suc n .Agda.Builtin.Equality.≡ m + m * n
  /-cong  : {i j : ℕ} (k : ℕ) → i + k * i ∣ j + k * j → i ∣ j
  distribʳ-*-+
          : (m n o : ℕ) → (n + o) * m .Agda.Builtin.Equality.≡ n * m + o * m
  im≡jm+n⇒[i∸j]m≡n
          : (i j m n : ℕ) →
            i * m .Agda.Builtin.Equality.≡ j * m + n →
            (i ∸ j) * m .Agda.Builtin.Equality.≡ n
  isCommutativeSemiring
          : .Algebra.Structures.IsCommutativeSemiring
            .Agda.Builtin.Equality._≡_ _+_ _*_ 0 1
  nonZeroDivisor-lemma
          : (m q : ℕ) (r : .Data.Fin.Fin (suc m)) →
            .Data.Fin.toℕ r .Relation.Binary.Core.≢ 0 →
            suc m ∣ .Data.Fin.toℕ r + q * suc m → .Data.Empty.⊥

Agda: Vector Membership in Stdlib? (And how to learn stdlib in general)

1 Answers