diff options
| author | Andreas Grois <andi@grois.info> | 2023-12-09 16:34:30 +0100 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2023-12-09 16:34:30 +0100 |
| commit | ecbf7b27be05dc242f066e681dbe22c4274834f5 (patch) | |
| tree | cab87543d89619e18da875a2435f2c1c6da9acdd /Common/List.lean | |
| parent | 244078f9f9e722aceafe64e745b9aa50136fb71a (diff) | |
Day 8 Part 2
Diffstat (limited to 'Common/List.lean')
| -rw-r--r-- | Common/List.lean | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/Common/List.lean b/Common/List.lean index 5d82e89..72ce808 100644 --- a/Common/List.lean +++ b/Common/List.lean @@ -36,19 +36,6 @@ def scan {α σ : Type} (step : σ → α → σ) (init : σ): List α → List 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 - def compare {α : Type} [Ord α] (a b : List α) := match a, b with | _ :: _, [] => Ordering.gt | [], _ :: _ => Ordering.lt |
