Agda：Stdlibのベクトルメンバーシップ？ （そして、一般的にstdlibを学ぶ方法）

Question

私はAgdaの文字列を扱っています。私はそれらのベクトルを持っています。私は、与えられた文字列がベクトル内に存在するかどうかをチェックする必要があります（変数が空文字列かどうかを調べる一環として、PL理論wprkでやっています）。

私はまだ標準ライブラリの周りを見つけていますが、私は他の言語（Haskellなど）の標準ライブラリにある基本的な機能を探しています。 。など

1. 標準ライブラリ内のベクトルのためのメンバーシップ関数があり、言語とその概念ではなく、私はAgdaで印加されるプログラミング、共通ライブラリを見てきた多くのことを学ぶための素晴らしいリソースは、あります、または1つを構築するための簡単な1つのライナー、または私は自分自身の関数を記述する必要がありますか？ （明らかにそのような関数は、要素型の決定可能な等価性に対してパラメータ化されます）

2. Agdaで標準ライブラリをどのように学びますか？良いガイドやチュートリアル、またはホグルのようなツールがありますか？

Answer 1

1を構築するための標準ライブラリ、または簡単なワンライナーでベクトルのメンバーシップ関数があり、または私は機能を自分で書く必要があるのですか？

これはわかりません。 right notionsはそこにありますが、検索機能AFAICTはありません。私が残りの答えで説明するコマンドを使用しても結果は得られません。

Agdaで標準ライブラリをどのように学びますか？良いガイドやチュートリアル、またはホグルのようなツールがありますか？

emacsの内部では、C-c C-zを使用してスコープ内の定義を検索できます。両方の識別子（型を記述した定義を選択します）と文字列リテラル（識別子にその文字列が含まれているものを選択します）を使用できます。

結果として、図書館を探索する1つの方法は、多くのモジュールをopen importにして、慎重に選択したキーワードにC-c C-zを使用することです。例えば。以下のモジュールで

module Explore where 

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

キーストロークC-c C-z _*_ _+_ RETリターン：

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.⊥