The lowering of `program`, whose launch declares `registers` registers
and whose plain shared accesses address memory as `addressing` says.
2536def sm121LowerWith =
2537 (lambda unrestricted addressing : (family SM121SharedAddressing) .
2538 (lambda unrestricted program : (family SM86Program) .
2539 (lambda unrestricted registers : Nat .
2540 (let unrestricted decoded = (sm121LowerDecodeProgram program) in
2541 (eliminate
2542 SM121LowerDecodedList
2543 (lambda unrestricted current : (family SM121LowerDecodedList) . (family SM121LowerResult))
2544 decoded
2545 (branch SM121LowerDecodedEnd . (sm121LowerFinish addressing decoded registers))
2546 (branch SM121LowerDecodedNext item tail induction . (sm121LowerFinish addressing decoded registers))
2547 (branch SM121LowerDecodedRefused refusal .
2548 (constructor SM121LowerResult SM121LowerRefused refusal)))))))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.