From 5a6ac7f4da9bc2d7f2cfb769d65db5db2da5da3e Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 21 Aug 2015 13:48:02 +0200
Subject: [PATCH] Annotate proof DSL as @library
---
library/proof/Internal.scala | 2 ++
library/proof/package.scala | 7 +++++++
2 files changed, 9 insertions(+)
diff --git a/library/proof/Internal.scala b/library/proof/Internal.scala
index 3ac290310..72333c501 100644
--- a/library/proof/Internal.scala
+++ b/library/proof/Internal.scala
@@ -2,8 +2,10 @@
package leon.proof
import leon.lang._
+import leon.annotation._
/** Internal helper classes and methods for the 'proof' package. */
+@library
object Internal {
/*** Helper classes for relational reasoning ***/
diff --git a/library/proof/package.scala b/library/proof/package.scala
index fd07a8128..f298dce27 100644
--- a/library/proof/package.scala
+++ b/library/proof/package.scala
@@ -9,6 +9,7 @@ import leon.proof.Internal._
package object proof {
+ @library
case class ProofOps(prop: Boolean) {
def because(proof: Boolean): Boolean = proof && prop
def neverHolds: Boolean = {
@@ -17,13 +18,17 @@ package object proof {
}
}
+ @library
implicit def boolean2ProofOps(prop: Boolean): ProofOps = ProofOps(prop)
+ @library
def trivial: Boolean = true
+ @library
def by(proof: Boolean)(prop: Boolean): Boolean =
proof && prop
+ @library
def check(prop: Boolean): Boolean = {
require(prop)
prop
@@ -39,6 +44,7 @@ package object proof {
* x
* }.qed
*/
+ @library
case class RelReasoning[A](x: A, prop: Boolean) {
def ^^[B](r: (A, B) => Boolean): WithRel[A, B] = WithRel(x, r, prop)
@@ -52,6 +58,7 @@ package object proof {
def qed: Boolean = prop
}
+ @library
implicit def any2RelReasoning[A](x: A): RelReasoning[A] =
RelReasoning(x, true)
--
GitLab