module Stdlib.Data.List;
open import Stdlib.Data.List.Base public;
open import Stdlib.Data.Bool.Base;
open import Stdlib.Data.String.Base;
open import Stdlib.Debug.Fail;
import Stdlib.Trait.Eq as Eq;
open Eq using {Eq};
import Stdlib.Trait.Ord as Ord;
open Ord using {Ord};
import Stdlib.Trait.Show as Show;
open Show using {Show};
--- 𝒪(1). Partial function that returns the first element of a ;List;.
head : {A : Type} → List A → A;
head (x :: _) := x;
head nil := fail "head: empty list";
--- 𝒪(𝓃 * 𝓂). Partial function that transposes a ;List; of ;List;s interpreted as a matrix.
terminating
transpose : {A : Type} → List (List A) → List (List A);
transpose (nil :: _) := nil;
transpose xss := map head xss :: transpose (map tail xss);
module ListTraits;
Eq : {A : Type} -> Eq A -> Eq (List A);
Eq {A} (Eq.mkEq eq-a) :=
let
go : List A -> List A -> Bool;
go nil nil := true;
go nil _ := false;
go _ nil := false;
go (x :: xs) (y :: ys) := if (eq-a x y) (go xs ys) false;
in Eq.mkEq go;
Ord : {A : Type} -> Ord A -> Ord (List A);
Ord {A} (Ord.mkOrd cmp-a) :=
let
go : List A -> List A -> Ord.Ordering;
go nil nil := Ord.EQ;
go nil _ := Ord.LT;
go _ nil := Ord.GT;
go (x :: xs) (y :: ys) :=
case cmp-a x y
| Ord.LT := Ord.LT
| Ord.GT := Ord.GT
| Ord.EQ := go xs ys;
in Ord.mkOrd go;
Show : {A : Type} -> Show A -> Show (List A);
Show {A} (Show.mkShow to-str) :=
let
go : List A -> String;
go nil := "nil";
go (x :: xs) := to-str x ++str " :: " ++str go xs;
in Show.mkShow
λ {
| nil := "nil"
| s := "(" ++str go s ++str ")"
};
end;
Last modified on 2023-05-08 11:40 UTC