80def finiteWordCheck =
81 (lambda unrestricted half : Nat .
82 (lambda unrestricted tail : (family X86NativeAssembly) .
83 (nat-eliminate (lambda unrestricted mode : Nat . (family X86NativeAssembly))
84 (finiteAnd finiteRAX 2139095040
85 (finiteCompare finiteRAX 2139095040
86 (finiteBranch (constructor X86NativeCondition X86NativeConditionZero)
87 b"reject" tail)))
88 (lambda unrestricted predecessor : Nat .
89 (lambda unrestricted unused : (family X86NativeAssembly) .
90 (finiteMove finiteRCX finiteRAX
91 (finiteAnd finiteRAX 32640
92 (finiteCompare finiteRAX 32640
93 (finiteBranch (constructor X86NativeCondition X86NativeConditionZero)
94 b"reject"
95 (finiteEmit (constructor X86NativeInstruction
96 X86NativeShiftRightImmediate64 finiteRCX
97 (constructor X86NativeImmediate8 X86NativeImmediate8Value (byte 16)))
98 (finiteAnd finiteRCX 32640
99 (finiteCompare finiteRCX 32640
100 (finiteBranch (constructor X86NativeCondition X86NativeConditionZero)
101 b"reject" tail))))))))))
102 half)))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.