From 559e944951bfb23f32556aecbfd366b7c39a91c7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Thu, 14 Apr 2016 19:58:59 +0200
Subject: [PATCH] Updated isabelle annotation for the new string theory.
---
library/theories/String.scala | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/library/theories/String.scala b/library/theories/String.scala
index 8cfced9d8..ca2b9027d 100644
--- a/library/theories/String.scala
+++ b/library/theories/String.scala
@@ -36,7 +36,8 @@ object String {
def fromChar(i: Char): String = {
StringCons(i, StringNil())
}
-
+
+ @isabelle.noBody()
def fromBigInt(i: BigInt): String =
if(i < 0) StringCons('-', fromBigInt(-i))
else if(i == BigInt(0)) StringCons('0', StringNil())
@@ -51,6 +52,7 @@ object String {
else if(i == BigInt(9)) StringCons('9', StringNil())
else fromBigInt(i / 10).concat(fromBigInt(i % 10))
+ @isabelle.noBody()
def fromInt(i: Int): String = i match {
case -2147483648 => StringCons('-', StringCons('2', fromInt(147483648)))
case i if i < 0 => StringCons('-', fromInt(-i))
--
GitLab