Skip to content

Make abstract quiet time bool

Sergey Bozhko requested to merge sbozhko/rt-proofs:quiet_time_bool into master

In the lemma I'm working on now, I need a bool version of this definition. As we discussed, we should avoid two identical versions (Prop + bool) whenever possible. So, this MR makes the quiet time def. to be bool

Merge request reports