feat: add some useful helper functions I didn't actually use in the end

This commit is contained in:
Sebastian Ullrich 2020-03-19 12:13:56 +01:00 committed by Leonardo de Moura
parent 3e7bc07f19
commit e999fa678d
2 changed files with 18 additions and 0 deletions

View file

@ -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

View file

@ -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