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