1877def greedyArgmaxSM86BuildValidated =
1878 (lambda unrestricted vocabulary : Nat .
1879 (app
1880 (lambda unrestricted program : (family SM86Program) .
1881 (app
1882 (lambda unrestricted manifest : (family GreedyArgmaxSM86Manifest) .
1883 (eliminate
1884 GreedyArgmaxSM86Manifest
1885 (lambda unrestricted current : (family GreedyArgmaxSM86Manifest) .
1886 (family GreedyArgmaxSM86Artifact))
1887 manifest
1888 (branch
1889 GreedyArgmaxSM86ManifestValue
1890 manifestVocabulary
1891 fullSlots
1892 tailLanes
1893 expectedInstructions
1894 expectedBytes
1895 registers
1896 sharedBytes
1897 gridX
1898 threads
1899 activeLoads
1900 activeFinite
1901 inactiveFinite
1902 tailMasks
1903 tieStages
1904 tokenWrites
1905 validityWrites
1906 hostReads
1907 fallbacks
1908 abi
1909 .
1910 (nat-eliminate
1911 (lambda unrestricted fallbackFree : Nat . (family GreedyArgmaxSM86Artifact))
1912 (greedyArgmaxSM86Failed
1913 manifest
1914 (constructor GreedyArgmaxSM86FailureCode GreedyArgmaxSM86HostFallbackDetected)
1915 fallbacks
1916 (sm86ProgramCount program)
1917 zero)
1918 (lambda unrestricted fallbackPredecessor : Nat .
1919 (lambda unrestricted fallbackInduction : (family GreedyArgmaxSM86Artifact) .
1920 (nat-eliminate
1921 (lambda unrestricted programExact : Nat . (family GreedyArgmaxSM86Artifact))
1922 (greedyArgmaxSM86Failed
1923 manifest
1924 (constructor
1925 GreedyArgmaxSM86FailureCode
1926 GreedyArgmaxSM86InstructionCountMismatch)
1927 (sm86ProgramCount program)
1928 (sm86ProgramCount program)
1929 zero)
1930 (lambda unrestricted programPredecessor : Nat .
1931 (lambda unrestricted programInduction : (family GreedyArgmaxSM86Artifact) .
1932 (greedyArgmaxSM86BuildEncoded program manifest)))
1933 (naturalEqual (sm86ProgramCount program) expectedInstructions))))
1934 (naturalEqual fallbacks zero)))))
1935 (greedyArgmaxSM86ManifestFor vocabulary)))
1936 (greedyArgmaxSM86ProgramFor vocabulary)))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.