A program's instructions decoded against its SM86 encoding
(Accelerator.SM86's sm86EncodeProgram, the words its canonical placement
holds), sixteen bytes each.
1224def sm121LowerDecodeProgram =
1225 (lambda unrestricted program : (family SM86Program) .
1226 (eliminate
1227 SM86ProgramEncodingResult
1228 (lambda unrestricted current : (family SM86ProgramEncodingResult) . (family SM121LowerDecodedList))
1229 (sm86EncodeProgram program)
1230 (branch SM86ProgramEncodingSucceeded image telemetry .
1231 (app
1232 (eliminate
1233 SM86Program
1234 (lambda unrestricted current : (family SM86Program) .
1235 (pi unrestricted words : Bytes . (family SM121LowerDecodedList)))
1236 program
1237 (branch SM86ProgramEnd .
1238 (lambda unrestricted words : Bytes . (constructor SM121LowerDecodedList SM121LowerDecodedEnd)))
1239 (branch SM86ProgramNext head tail induction .
1240 (lambda unrestricted words : Bytes .
1241 (constructor SM121LowerDecodedList SM121LowerDecodedNext
1242 (sm121LowerDecode head words)
1243 (induction (sm121LowerDrop sm121LowerInstructionBytes words))))))
1244 image))
1245 (branch SM86ProgramEncodingFailed ordinal failure telemetry .
1246 (constructor SM121LowerDecodedList SM121LowerDecodedRefused
1247 (constructor SM121LowerRefusal SM121LowerRefusedEncoding)))))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.