From c4f8ce7fcac178c963cd59f2efe7f0ff13004085 Mon Sep 17 00:00:00 2001
From: Lars Hupel <lars.hupel@mytum.de>
Date: Fri, 6 May 2016 18:21:18 +0200
Subject: [PATCH] disable bodies for `takeI`/`dropI`
Isabelle can't prove termination for those methods which have been
introduced in 61c7302.
---
library/theories/String.scala | 2 ++
1 file changed, 2 insertions(+)
diff --git a/library/theories/String.scala b/library/theories/String.scala
index 8057c2d2a..541e90261 100644
--- a/library/theories/String.scala
+++ b/library/theories/String.scala
@@ -30,11 +30,13 @@ sealed abstract class String {
case _ => this
}
+ @isabelle.noBody()
def takeI(i: Int): String = this match {
case StringCons(head, tail) if i > 0 => StringCons(head, tail takeI (i - 1))
case _ => StringNil()
}
+ @isabelle.noBody()
def dropI(i: Int): String = this match {
case StringCons(head, tail) if i > 0 => tail dropI (i - 1)
case _ => this
--
GitLab