until -package:numeric-prelude -package:intro -package:classy-prelude -package:rebase -package:termonad -package:extra -package:streaming package:copilot-libraries

until n s0 s1 means that eventually n s1, and up until at least the period before s1 holds, s0 continuously holds. Note: Both argument streams must have sufficient history to drop n values from them.
True until another stream is true, within the time bounds specified. until l u clk dist s0 s1 is true at time t iff there exists a d, with l <= d <= u, such that s1 is true at time (t + d), and for all times t' with t <= t' < t + d, s0 is true at those times.
Matching Until: Same semantics as until, except with both s1 and s0 needing to hold at time (t + d) instead of just s1.