Agda 标准库列表最大值

Question

我正在尝试获取 Data.List:

的最大元素

listMax : max ℕ (2 ∷ 1 ∷ []) ≟ 2
listMax = ?

但不明白为什么会出现此错误：

Set !=< (Relation.Binary.Bundles.TotalOrder _b_20 _ℓ₁_21 _ℓ₂_22)
when checking that the expression ℕ has type
Relation.Binary.Bundles.TotalOrder _b_20 _ℓ₁_21 _ℓ₂_22

我猜 ℕ 应该是某种类型的东西 Relation.Binary.Bundles.TotalOrder _b_20 _ℓ₁_21 _ℓ₂_22 但我不知道如何获得那种类型的东西以及为什么需要它来获得最大元素。

编辑

查看 Data.List.Extrema 中 max 的签名，我看到：

max : B → List B → B

我看到这里定义了 B

open TotalOrder totalOrder renaming (Carrier to B)

我不确定为什么 ℕ 不能成为承运人。

我也在Data.Fin.Properties中找到：

≤-totalOrder : ℕ → TotalOrder _ _ _

尝试过

listMax : {n : ℕ} → max (≤-totalOrder n) (2 l.∷ 1 l.∷ l.[]) ≡ 2

但我现在收到此错误：

List _A_27 !=< Fin n
when checking that the inferred type of an application
  List _A_27
matches the expected type
  Relation.Binary.Bundles.TotalOrder.Carrier (≤-totalOrder n)

谢谢！

Answer 1

在Data.String.Base中找到这个例子后：

rectangle : ∀ {n} → Vec (ℕ → String → String) n →
            Vec String n → Vec String n
rectangle pads cells = Vec.zipWith (λ p c → p width c) pads cells where

  sizes = List.map length (Vec.toList cells)
  width = max 0 sizes

我发现对 max 的调用应该类似于

max 0 (2 l.∷ l.[])

还发现我遗漏了导入：

open import Data.List.Extrema ℕₚ.≤-totalOrder

由于我还不知道的原因，使用此导入不会出现错误：

ℕ != (Relation.Binary.TotalOrder _b_26 _ℓ₁_27 _ℓ₂_28)
when checking that the expression 0 has type
Relation.Binary.TotalOrder _b_26 _ℓ₁_27 _ℓ₂_28

我从这个导入中得到的：

open import Data.List.Extrema (max)

我仍然很好奇导入的原因

open import Data.List.Extrema ℕₚ.≤-totalOrder

工作。

Agda 标准库列表最大值

Agda stdlib List max

list

agda