Skip to content

Commit

Permalink
Move forall and exists to the SetOps class
Browse files Browse the repository at this point in the history
  • Loading branch information
samuelchassot committed Oct 16, 2024
1 parent 4d18542 commit 0897b25
Showing 1 changed file with 11 additions and 3 deletions.
14 changes: 11 additions & 3 deletions frontends/library/stainless/lang/Set.scala
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,17 @@ object Set {
@library
implicit class SetOps[A](val set: Set[A]) extends AnyVal {


@extern @pure
def exists(p: A => Boolean): Boolean = {
set.theSet.exists(p)
}

@extern @pure
def forall(p: A => Boolean): Boolean = {
set.theSet.forall(p)
}

@extern @pure
def map[B](f: A => B): Set[B] = {
new Set(set.theSet.map(f))
Expand Down Expand Up @@ -126,7 +137,4 @@ sealed case class Set[T](theSet: scala.collection.immutable.Set[T]) {

def contains(a: T): Boolean = theSet.contains(a)
def subsetOf(b: Set[T]): Boolean = theSet.subsetOf(b.theSet)

def exists(p: T => Boolean): Boolean = theSet.exists(p)
def forall(p: T => Boolean): Boolean = theSet.forall(p)
}

0 comments on commit 0897b25

Please sign in to comment.