Source/Reference

SM86.Scoreboard

reference/target-models/checked/SM86/Scoreboard.alpha

437 lines42 declarations25.5 KiBSHA-256 e8d85751fb4f

def · lines 238–242

sbRegistersNonempty

Full file
238def sbRegistersNonempty =
239  (lambda unrestricted registers : (family StdList Nat) .
240    (eliminate StdList (lambda unrestricted current : (family StdList Nat) . Nat) registers
241      (branch StdListEmpty . 0)
242      (branch StdListCons register tail induction . 1)))

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.