The SM86 indices branches in `decoded` jump to.
2089def sm121LowerBranchTargets =
2090 (lambda unrestricted decoded : (family SM121LowerDecodedList) .
2091 (sm121LowerDecodedFoldIndexed (family SM121LowerRegisters) decoded sm121LowerNone
2092 (lambda unrestricted targets : (family SM121LowerRegisters) .
2093 (lambda unrestricted index : Nat .
2094 (lambda unrestricted item : (family SM121LowerDecoded) .
2095 (eliminate
2096 SM121LowerDecoded
2097 (lambda unrestricted current : (family SM121LowerDecoded) . (family SM121LowerRegisters))
2098 item
2099 (branch SM121LowerDecodedValue low high guardReads shape .
2100 (eliminate
2101 SM121LowerShape
2102 (lambda unrestricted current : (family SM121LowerShape) . (family SM121LowerRegisters))
2103 shape
2104 (branch SM121LowerShapeValue rule class reads writes predicateWrites .
2105 (let unrestricted mark = (sm121LowerBranchTarget low high index) in
2106 (sm121LowerSelect (family SM121LowerRegisters)
2107 (naturalAnd (sm121LowerIsBranchRule rule) (naturalIsZero (naturalIsZero mark)))
2108 (sm121LowerCons (nat-subtract mark 1) targets)
2109 targets)))))))))))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.