vector - Agda:Stdlib 中的向量成员资格？ (以及一般如何学习 stdlib)

Question

我在 Agda 中处理字符串，并且我有它们的向量。我需要检查给定字符串是否出现在向量中(作为检查变量是否自由或绑定(bind)在表达式中的一部分，在我正在做的 PL 理论 wprk 中)。

我仍在寻找标准库的出路，我发现我花了很多时间寻找其他语言(Haskell 等)的标准库中的基本函数。有很多学习语言及其概念的资源，但我在 Agda、公共(public)库等中看到的应用程序编程资源并不多。

1. 标准库中是否有 Vectors 的隶属函数，或者是否有简单的一行代码来构造一个，或者我是否需要自己编写该函数？ (显然，这样的函数将根据元素类型的可判定相等性进行参数化)

2. 你是如何学习 Agda 中的标准库的？是否有好的指南/教程或类似 hoogle 的工具？

Answer 1

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?

据我所知没有。 right notions有但没有搜索功能 AFAICT。使用我在其余答案中描述的命令不会产生任何结果。

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

在 emacs 中，您可以使用 C-c C-z 来搜索范围内的定义。您可以同时使用标识符(它将选择其类型提及它们的定义)和字符串文字(它将选择其标识符包含该字符串的定义)。

因此，探索该库的一种方法是打开导入 大量模块并在精心选择的关键字上使用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.⊥