The wait mask naming each scoreboard `barriers` holds, and `freeBarrier`.
1298def sm121LowerWaitAllOf =
1299 (lambda unrestricted barriers : (family SM121LowerMask) .
1300 (lambda unrestricted freeBarrier : Nat .
1301 (nat-eliminate
1302 (lambda unrestricted current : Nat . Nat)
1303 zero
1304 (lambda unrestricted barrier : Nat .
1305 (lambda unrestricted induction : Nat .
1306 (nat-add induction
1307 (naturalSelect
1308 (naturalOr (sm121LowerMaskHas barriers barrier) (naturalEqual barrier freeBarrier))
1309 (sm121LowerPlace barrier)
1310 zero))))
1311 sm121LowerBarrierCount)))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.