Aww, I was hoping you were going to use NoOverdrafts to then show how the spec could instead be written by including NoOverdrafts in the spec itself to obviate the upper bound in the transfer spec itself, i.e. some value in 1..=alice[t] can then turn into just some value in 1...
Aww, I was hoping you were going to use
NoOverdraftsto then show how the spec could instead be written by includingNoOverdraftsin the spec itself to obviate the upper bound in the transfer spec itself, i.e.some value in 1..=alice[t]can then turn into justsome value in 1...