Agda：Stdlib中的向量成员？（以及如何通常学习stdlib）

我正在处理Agda中的字符串，并且我已经有了它们的向量。我需要检查一个给定的字符串是否出现在一个向量中（作为检查一个变量是否在表达式中自由或绑定的一部分，在PL理论wprk中我正在做）。Agda：Stdlib中的向量成员？（以及如何通常学习stdlib）

我仍在寻找围绕标准库的方法，而且我发现我花费大量时间寻找其他语言的标准库（Haskell等）中的基本函数，。有学习语言和它的概念，但不是说我已经看到了在阿格达应用程序，公共库了很多伟大的资源等

是否有标准库向量隶属函数，或者简单的一行来构建一个，还是我需要自己编写函数？（显然这样的功能将被参数化为对于元素类型的可判定的相等性）
你如何学习Agda的标准库？有很好的指南/教程，或者一个类似hoogle的工具吗？

来源

2017-03-06 jmite

是否有标准库的向量隶属函数，或者一个简单的一行来构造一个，或者我需要写函数自己？

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

你如何学习Agda的标准库？有很好的指南/教程，或者一个类似hoogle的工具吗？

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

来源

2017-03-07 03:15:17 gallais

Agda：Stdlib中的向量成员？ （以及如何通常学习stdlib）

回答

相关问题

Agda：Stdlib中的向量成员？（以及如何通常学习stdlib）