each of `registers` now on `barrier` (its earlier entry replaced)
2201def sm121LowerBoardsAdd =
2202 (lambda unrestricted boards : (family SM121LowerBoards) .
2203 (lambda unrestricted registers : (family SM121LowerRegisters) .
2204 (lambda unrestricted barrier : Nat .
2205 (eliminate
2206 SM121LowerRegisters
2207 (lambda unrestricted current : (family SM121LowerRegisters) . (family SM121LowerBoards))
2208 registers
2209 (branch SM121LowerRegistersEnd . boards)
2210 (branch SM121LowerRegistersNext head tail induction .
2211 (constructor SM121LowerBoards SM121LowerBoardsNext head barrier
2212 (sm121LowerBoardsRemove induction head)))))))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.