Construct to write invariant

src/main/scala/leon/Utils.scala

@@ -9,4 +9,10 @@ object Utils {
   }
 
   implicit def any2IsValid(x: Boolean) : IsValid = new IsValid(x)
+
+
+  object InvariantFunction {
+    def invariant(x: Boolean): Unit = ()
+  }
+  implicit def while2Invariant(u: Unit) = InvariantFunction
 }