1783def greedyArgmaxSM86BuildEncoded =
1784 (lambda unrestricted program : (family SM86Program) .
1785 (lambda unrestricted manifest : (family GreedyArgmaxSM86Manifest) .
1786 (eliminate
1787 SM86ProgramEncodingResult
1788 (lambda unrestricted current : (family SM86ProgramEncodingResult) .
1789 (family GreedyArgmaxSM86Artifact))
1790 (sm86EncodeProgram program)
1791 (branch
1792 SM86ProgramEncodingSucceeded
1793 image
1794 telemetry
1795 .
1796 (eliminate
1797 SM86ProgramEncodingTelemetry
1798 (lambda unrestricted current : (family SM86ProgramEncodingTelemetry) .
1799 (family GreedyArgmaxSM86Artifact))
1800 telemetry
1801 (branch
1802 SM86ProgramEncodingTelemetryValue
1803 instructions
1804 encodedBytes
1805 fields
1806 bits
1807 highest
1808 .
1809 (eliminate
1810 GreedyArgmaxSM86Manifest
1811 (lambda unrestricted current : (family GreedyArgmaxSM86Manifest) .
1812 (family GreedyArgmaxSM86Artifact))
1813 manifest
1814 (branch
1815 GreedyArgmaxSM86ManifestValue
1816 vocabulary
1817 fullSlots
1818 tailLanes
1819 expectedInstructions
1820 expectedBytes
1821 registers
1822 sharedBytes
1823 gridX
1824 threads
1825 activeLoads
1826 activeFinite
1827 inactiveFinite
1828 tailMasks
1829 tieStages
1830 tokenWrites
1831 validityWrites
1832 hostReads
1833 fallbacks
1834 abi
1835 .
1836 (nat-eliminate
1837 (lambda unrestricted instructionsExact : Nat .
1838 (family GreedyArgmaxSM86Artifact))
1839 (greedyArgmaxSM86Failed
1840 manifest
1841 (constructor
1842 GreedyArgmaxSM86FailureCode
1843 GreedyArgmaxSM86EncodedInstructionCountMismatch)
1844 instructions
1845 instructions
1846 encodedBytes)
1847 (lambda unrestricted instructionPredecessor : Nat .
1848 (lambda unrestricted instructionInduction : (family GreedyArgmaxSM86Artifact) .
1849 (nat-eliminate
1850 (lambda unrestricted bytesExact : Nat . (family GreedyArgmaxSM86Artifact))
1851 (greedyArgmaxSM86Failed
1852 manifest
1853 (constructor
1854 GreedyArgmaxSM86FailureCode
1855 GreedyArgmaxSM86EncodedByteCountMismatch)
1856 encodedBytes
1857 instructions
1858 encodedBytes)
1859 (lambda unrestricted bytePredecessor : Nat .
1860 (lambda unrestricted byteInduction : (family GreedyArgmaxSM86Artifact) .
1861 (greedyArgmaxSM86BuildIdentity program image manifest telemetry)))
1862 (naturalEqual encodedBytes expectedBytes))))
1863 (naturalEqual instructions expectedInstructions)))))))
1864 (branch
1865 SM86ProgramEncodingFailed
1866 instructionIndex
1867 failure
1868 telemetry
1869 .
1870 (greedyArgmaxSM86Failed
1871 manifest
1872 (constructor GreedyArgmaxSM86FailureCode GreedyArgmaxSM86ImageEncodingFailed)
1873 instructionIndex
1874 (sm86ProgramCount program)
1875 zero)))))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.