Agda: adhésion de vecteur dans Stdlib? (Et comment apprendre stdlib en général)

Question

J'ai affaire à des cordes dans Agda, et j'en ai un vecteur. J'ai besoin de vérifier si une chaîne donnée se produit dans un vecteur (dans le cadre de la vérification si une variable est libre ou liée dans une expression, dans la théorie de PL wprk que je fais). Je trouve encore mon chemin dans la bibliothèque standard et je trouve que je passe beaucoup de temps à chercher les fonctions de base qui seraient dans la bibliothèque standard dans d'autres langues (Haskell, etc.) . Il y a d'excellentes ressources pour l'apprentissage de la langue et de ses concepts, mais pas beaucoup que je l'ai vu pour la programmation appliquée dans Agda, bibliothèques communes, etc.

1. Y at-il une fonction d'appartenance pour les vecteurs dans la bibliothèque standard, ou un simple interligne pour en construire un, ou dois-je écrire la fonction moi-même? (De toute évidence, une telle fonction serait paramétrée sur l'égalité décidable pour le type d'élément)

2. Comment apprenez-vous la bibliothèque standard dans Agda? Y a-t-il de bons guides/tutoriels, ou un outil similaire à Hoogle?

Answer 1

Y at-il une fonction d'appartenance pour les vecteurs dans la bibliothèque standard, ou un one-liner facile à construire un, ou dois-je besoin d'écrire moi-même la fonction?

Pas que je sache. Les right notions sont là mais pas la fonction de recherche AFAICT. Et l'utilisation de la commande que je décris dans le reste de la réponse ne donne aucun résultat.

Comment apprenez-vous la bibliothèque standard dans Agda? Y a-t-il de bons guides/tutoriels, ou un outil similaire à Hoogle?

À l'intérieur d'emacs, vous pouvez utiliser C-c C-z pour rechercher les définitions incluses dans la portée. Vous pouvez utiliser les deux identifiants (il sélectionnera les définitions dont le type les mentionne) et les littéraux de chaîne (il sélectionnera ceux dont l'identificateur contient cette chaîne). Par conséquent, une façon d'explorer la bibliothèque est de open import beaucoup de modules et d'utiliser C-c C-z sur des mots-clés soigneusement sélectionnés. Par exemple. dans le module suivant

module Explore where 

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

les rendements de frappe 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.⊥