From e999fa678db6893f4aea1398fbc1dca234031677 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 19 Mar 2020 12:13:56 +0100
Subject: [PATCH] feat: add some useful helper functions I didn't actually use
 in the end

---
 src/Init/Data/List/Basic.lean   | 10 ++++++++++
 src/Init/Data/Option/Basic.lean |  8 ++++++++
 2 files changed, 18 insertions(+)

diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index 0a71a5396b..7f6c919068 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -201,6 +201,16 @@ eraseDupsAux as []
 @[inline] def span (p : α → Bool) (as : List α) : List α × List α :=
 spanAux p as []
 
+@[specialize] def groupByAux (eq : α → α → Bool) : List α → List (List α) → List (List α)
+| a::as, (ag::g)::gs => match eq a ag with
+  | true  => groupByAux as ((a::ag::g)::gs)
+  | false => groupByAux as ([a]::(ag::g).reverse::gs)
+| _, gs => gs.reverse
+
+@[specialize] def groupBy (p : α → α → Bool) : List α → List (List α)
+| []    => []
+| a::as => groupByAux p as [[a]]
+
 def lookup [HasBeq α] : α → List (α × β) → Option β
 | _, []        => none
 | a, (k,b)::es => match a == k with
diff --git a/src/Init/Data/Option/Basic.lean b/src/Init/Data/Option/Basic.lean
index b1c2f156e1..5a9c67694b 100644
--- a/src/Init/Data/Option/Basic.lean
+++ b/src/Init/Data/Option/Basic.lean
@@ -51,6 +51,14 @@ instance : Monad Option :=
 | some a => if p a then some a else none
 | none   => none
 
+@[inline] protected def all {α} (p : α → Bool) : Option α → Bool
+| some a => p a
+| none   => true
+
+@[inline] protected def any {α} (p : α → Bool) : Option α → Bool
+| some a => p a
+| none   => false
+
 @[macroInline] protected def orelse {α : Type u} : Option α → Option α → Option α
 | some a, _ => some a
 | none,   b => b