Skip to content
Snippets Groups Projects
Commit 55e0adfd authored by Manos Koukoutos's avatar Manos Koukoutos
Browse files

Strengthen List.apply spec

parent 15bd06d2
Branches
Tags
No related merge requests found
...@@ -62,6 +62,8 @@ sealed abstract class List[T] { ...@@ -62,6 +62,8 @@ sealed abstract class List[T] {
} else { } else {
tail(index-1) tail(index-1)
} }
} ensuring {
content.contains(_)
} }
@isabelle.function(term = "%xs x. x # xs") @isabelle.function(term = "%xs x. x # xs")
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment