Skip to content
Snippets Groups Projects
Commit c4f8ce7f authored by Lars Hupel's avatar Lars Hupel
Browse files

disable bodies for `takeI`/`dropI`

Isabelle can't prove termination for those methods which have been
introduced in 61c73029.
parent 95e3848e
Branches
Tags
No related merge requests found
...@@ -30,11 +30,13 @@ sealed abstract class String { ...@@ -30,11 +30,13 @@ sealed abstract class String {
case _ => this case _ => this
} }
@isabelle.noBody()
def takeI(i: Int): String = this match { def takeI(i: Int): String = this match {
case StringCons(head, tail) if i > 0 => StringCons(head, tail takeI (i - 1)) case StringCons(head, tail) if i > 0 => StringCons(head, tail takeI (i - 1))
case _ => StringNil() case _ => StringNil()
} }
@isabelle.noBody()
def dropI(i: Int): String = this match { def dropI(i: Int): String = this match {
case StringCons(head, tail) if i > 0 => tail dropI (i - 1) case StringCons(head, tail) if i > 0 => tail dropI (i - 1)
case _ => this case _ => this
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment