package stainless.lang

import stainless.annotation._

object StaticChecks {

  @library
  implicit class Ensuring[A](val x: A) extends AnyVal {
    def ensuring(@ghost cond: (A) => Boolean): A = x
  }

  @library @ignore
  implicit class WhileDecorations(val u: Unit) {
    def invariant(@ghost x: Boolean): Unit = {
      require(x)
      u
    }
  }

  @library
  def require(@ghost pred: Boolean): Unit = ()

  @library
  def assert(@ghost pred: Boolean): Unit = ()

}


package stainless.lang

import stainless.annotation._

object StaticChecks {

  @library
  implicit class Ensuring[A](val x: A) extends AnyVal {
    def ensuring(@ghost cond: (A) => Boolean): A = x
  }

  @library
  def require(@ghost pred: Boolean): Unit = ()

  @library
  def assert(@ghost pred: Boolean): Unit = ()

}


--- 
+++ 
@@ -9,6 +9,14 @@
     def ensuring(@ghost cond: (A) => Boolean): A = x
   }
 
+  @library @ignore
+  implicit class WhileDecorations(val u: Unit) {
+    def invariant(@ghost x: Boolean): Unit = {
+      require(x)
+      u
+    }
+  }
+
   @library
   def require(@ghost pred: Boolean): Unit = ()
 
Add while invariant with ghost argument
