diff options
Diffstat (limited to 'Common/List.lean')
| -rw-r--r-- | Common/List.lean | 26 |
1 files changed, 25 insertions, 1 deletions
diff --git a/Common/List.lean b/Common/List.lean index 4076c87..1a76c3e 100644 --- a/Common/List.lean +++ b/Common/List.lean @@ -1,3 +1,5 @@ +namespace List + theorem listFilterSmallerOrEqualList (l : List α) (p : α → Bool) : l.length ≥ (l.filter p).length := by induction l with | nil => simp[List.filter] @@ -10,7 +12,6 @@ theorem listFilterSmallerOrEqualList (l : List α) (p : α → Bool) : l.length assumption | true => simp_arith[hi] - def quicksort {α : Type} [Ord α] : List α → List α | [] => [] | a :: as => @@ -22,3 +23,26 @@ def quicksort {α : Type} [Ord α] : List α → List α let biggers := as.filter largerEqualPred (quicksort smallers) ++ [a] ++ (quicksort biggers) termination_by quicksort l => l.length + +/-- Maps a List to another list, but keeps state. + The output list is a list of the state, and **has** the initial state + prepended! + -/ +def scan {α σ : Type} (step : σ → α → σ) (init : σ): List α → List σ +| [] => [init] +| a :: as => + let next := step init a + init :: scan step next as + +/-- Removes repeated entries. [1,2,2,1] becomes [1,2,1]-/ +def dedup {α : Type} [BEq α] (input : List α) : List α := + let rec helper : List α → α → List α := λ + | [], _ => [] + | a :: as, b => + if a == b then + helper as a + else + a :: helper as a + match input with + | [] => [] + | a :: as => a :: helper as a |