From a6223ef46c0ebf1d6b874b7d3fb1f61ceb809f13 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 11 Sep 2015 16:38:54 +0200
Subject: [PATCH] Add @library annotation
---
library/monads/state/State.scala | 12 ++++++++----
1 file changed, 8 insertions(+), 4 deletions(-)
diff --git a/library/monads/state/State.scala b/library/monads/state/State.scala
index 8bdb38320..f6a887356 100644
--- a/library/monads/state/State.scala
+++ b/library/monads/state/State.scala
@@ -4,6 +4,7 @@ import leon.collection._
import leon.lang._
import leon.annotation._
+@library
case class State[S, A](runState: S => (A, S)) {
/** Basic monadic methods */
@@ -52,6 +53,7 @@ case class State[S, A](runState: S => (A, S)) {
}
+@library
object State {
@inline
@@ -148,7 +150,7 @@ object State {
}
-
+@library
object MonadStateLaws {
import State._
@@ -215,6 +217,7 @@ object MonadStateLaws {
}
+@library
object ExampleCounter {
import State._
@@ -222,6 +225,7 @@ object ExampleCounter {
def counter(init: BigInt) = {
@inline
+ @library
def tick = modify[BigInt](_ + 1)
init >:: (for {
@@ -232,10 +236,9 @@ object ExampleCounter {
} yield r)
} ensuring( _ == init + 3 )
-
-
}
+@library
object ExampleTicTacToe {
import State._
@@ -310,6 +313,7 @@ object ExampleTicTacToe {
//}.holds
}
+@library
object ExampleFreshen {
import State._
@@ -360,7 +364,7 @@ object ExampleFreshen {
}
-
+@library
object ExampleStackEval {
import State._
--
GitLab