ensures forall i {:trigger i in [Max(xs + ys)]} :: i in xs + ys ==> Max(xs + ys) >= i
In particular, the trigger looks a bit unusual. I would have expected it to be something along the lines {:trigger i in xs + ys}. Is there a specific reason as to why it is the way it is?
I hope this kind of question is fine to ask here as an issue.
Looking through src/Collections/Sequences/Seq.dfy I noted the following postcondition for
LemmaMaxOfConcat:In particular, the trigger looks a bit unusual. I would have expected it to be something along the lines
{:trigger i in xs + ys}. Is there a specific reason as to why it is the way it is?I hope this kind of question is fine to ask here as an issue.