Агда: Вектор Членство в Stdlib? (А как научить стдлиб вообще)

Question

Я имею дело со строками в Агде, и у меня есть их вектор. Мне нужно проверить, встречается ли данная строка в векторе (как часть проверки, является ли переменная свободной или связанной в выражении, в теории PL, которую я делаю wprk).

Я все еще пытаюсь обойти стандартную библиотеку и обнаружил, что трачу много времени на поиск базовых функций, которые были бы в стандартной библиотеке на других языках (Haskell и т. Д.). Есть большие ресурсы для изучения языка и его концепций, но не так много, что я видел для прикладного программирования в Agda, общих библиотеках и т. Д.

1. Есть ли функция принадлежности для Векторов в стандартной библиотеке или простая однострочная для ее создания, или мне нужно написать функцию самостоятельно? (Очевидно, что такая функция будет параметризована по разрешимому равенству для типа элемента)

2. Как вы изучаете стандартную библиотеку в Агде? Есть ли хорошие руководства / учебные пособия или инструмент, похожий на Google?

Answer 1

Есть ли функция принадлежности для Векторов в стандартной библиотеке или простая однострочная для ее создания, или мне нужно написать функцию самостоятельно?

Не то, что я знаю из. Правильные понятия есть, но нет функции поиска AFAICT. И использование команды, которую я опишу в оставшейся части ответа, не даст никакого результата.

Как вы изучаете стандартную библиотеку в Агде? Есть ли хорошие руководства / учебные пособия или инструмент, похожий на Google?

Внутри Emacs вы можете использовать C-c C-z искать определения в объеме. Вы можете использовать как идентификаторы (он будет выбирать определения, чей тип упоминает их), так и строковые литералы (он будет выбирать те, чей идентификатор содержит эту строку).

Как следствие, одним из способов изучения библиотеки является 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.⊥