Agda stdlib List max

0
votes

I'm trying to get the max element of a Data.List:

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

but don't understand why I'm getting this error:

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

I'm guessing that ℕ should instead be something of type Relation.Binary.Bundles.TotalOrder _b_20 _ℓ₁_21 _ℓ₂_22 but I don't know how to get something of that type and why is it needed to get the max element.

EDIT

Looking at the signature for max in Data.List.Extrema I see:

max : B → List B → B

and I see that B is defined here

open TotalOrder totalOrder renaming (Carrier to B)

I'm not sure why ℕ can't be a Carrier.

I also found in Data.Fin.Properties:

≤-totalOrder : ℕ → TotalOrder _ _ _

and tried

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

but am now getting this error:

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)

Thanks!

1
listagda

1 Answers

0
votes

After finding this example in 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

I found out that the call to max should look like

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

and also found that I was missing the import:

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

For a reason I don't yet know, using this import doesn't give the error:

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

that I was getting from doing this import:

open import Data.List.Extrema (max)

I'm still curious as to what makes the import

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

work.