|
Lemma setUitv1 a x b : (a <= BLeft x)%O -> |
Following with remark by @t6s in the conversation of the PR #1848 :
One bad thing about this generalization is that all use cases of setUitv1 and setU1itv in analysis master
are backwards rewriting, and adding another parameter b breaks them.
Yes, in fact it is not very pleasant to use because one has to think about the meaning of the boolean flags
each time and there are difficult to remember. I think that there should be aliases with easy to understand names to facilitate usage.
analysis/classical/set_interval.v
Line 186 in e9a1231
Following with remark by @t6s in the conversation of the PR #1848 :
Yes, in fact it is not very pleasant to use because one has to think about the meaning of the boolean flags
each time and there are difficult to remember. I think that there should be aliases with easy to understand names to facilitate usage.