Conversation
…y selected trigger
parno
left a comment
parno
left a comment
There was a problem hiding this comment.
A few minor suggestions. I think we had also discussed updating the README or STYLE file with a note along the lines of "The {:trigger} annotations used in the standard library are an advanced topic and should not be needed when starting out on Dafny projects."
|
Cool, thanks for the changes! |
RustanLeino
left a comment
RustanLeino
left a comment
There was a problem hiding this comment.
Nice! Thank you. It really good to see so many manual triggers go. I have a few specific comments below.
| /* Dafny selected triggers: {x in xs}, {x in m}, {x in m'} */ | ||
| ensures forall x {:trigger x in m'} :: x in m' ==> x in m && x !in xs |
There was a problem hiding this comment.
The trigger in the other direction (that is, x in m) seems equally useful to me. Is there a reason not to include it?
There was a problem hiding this comment.
Since the ensures is an implication, we might only want the x in m'? My limited understanding is that we are ensuring the properties of m', rather than the original m. So might not be necessary to invoke this fact every time we see the original map.
|
@RustanLeino I believe Yi has addressed all of the issues you raised. Is this ready to be merged? |
3 participants
removed some tiggers that repeats dafny's selection
added some comments for dafny selected trigger