Change decreases _ to decreases + Add body

seqs/seqs.gobra

@@ -137,7 +137,7 @@ ghost
 requires 0 <= a1 && a1 <= b1 && b1 <= len(xs)
 requires 0 <= a2 && a2 <= b2 && b2 <= a1 - b1
 ensures xs[a1:b1][a2:b2] == xs[a1+a2:b1+b2]
-decreases _
+decreases
 pure func SubseqOfSubseq(xs seq[int], a1, b1, a2, b2 int) util.Unit {
 	return util.Unit{}
 }
@@ -292,7 +292,7 @@ ensures len(result) == len(xs) + 1
 ensures forall i int :: { result[i] } { xs[i] } (0 <= i && i < pos) ==> result[i] == xs[i]
 ensures result[pos] == e
 ensures forall i int :: { xs[i] } (pos <= i && i < len(xs)) ==> result[i+1] == xs[i]
-decreases _
+decreases
 pure func Insert(xs seq[int], e int, pos int) (result seq[int]) {
 	return xs[:pos] ++ Singleton(e) ++ xs[pos:]
 }

util/util.gobra

@@ -22,22 +22,22 @@ const Uncallable bool = false
 
 ghost
 requires false
-decreases _
-func Unreachable()
+decreases
+func Unreachable() { }
 
 ghost
 ensures false
-decreases _
+decreases
 func IgnoreBranch()
 
 ghost
 ensures false
-decreases _
+decreases
 func TODO()
 
 ghost
 requires b
-decreases _
+decreases
 pure func Asserting(ghost b bool) Unit {
 	return Unit{}
 }