ListSet implementation.#822
Conversation
jad-hamza
left a comment
jad-hamza
left a comment
There was a problem hiding this comment.
Thank you for the nice additions! I commented on a few minor things, and I would try to make the lemmas and specifications be less dependent on the forall quantifier which is not stable at the moment.
| }.ensuring(_ ⇒ first.contains(elem) ==> second.contains(elem)) | ||
|
|
||
| @opaque | ||
| def transitivePredicate[T](elem: T, list: T ⇒ Boolean, p: T => Boolean): Unit = { |
There was a problem hiding this comment.
Strange lemma :) Is it really needed?
There was a problem hiding this comment.
I need it here, filteringWithExpandingPredicateCreatesSubsets not sure why isn't it obvious.
|
Looks like the build is stuck even though all tests passed. |
The two builds might have been killed due to memory or time usage, can we increase the limits? |
Yeah, it should be possible. The memory limit is hard-coded in the larabot code here. Someone should also investigate why the build doesn't get killed correctly and end in failure. |
OStevan
force-pushed
the
ostevan/lis-set
branch
from
d755e3a to
7a46bba
Compare
jad-hamza
force-pushed
the
ostevan/lis-set
branch
3 times, most recently
from
d55d4ab to
77bdc27
Compare
jad-hamza
force-pushed
the
ostevan/lis-set
branch
from
77bdc27 to
c470a83
Compare
|
Going forward, we are trying to not use non-bounded foralls and we try to put the data structures into https://github.com/epfl-lara/bolts/ whenever they are not treated specially in front end extraction. |
|
@samuelchassot we should check if we should put this into bolts/data-structures and if we can get some of it using set.toList functionality in stainless library. |
5 participants
ListSetimplementation with some basic functionality. Along with this there are additional proofs forLists. Any suggestions regarding changes in naming and proof generalization are welcome.