Compiler.MachineX86NativeAssembly

67def x86NativeLookupLabel :
68  (pi unrestricted name : Bytes .
69    (pi unrestricted table : (family X86NativeLabelTable) . (family X86NativeLabelLookupResult))) =
70  (lambda unrestricted name : Bytes .
71    (lambda unrestricted table : (family X86NativeLabelTable) .
72      (eliminate
73        X86NativeLabelTable
74        (lambda unrestricted value : (family X86NativeLabelTable) .
75          (family X86NativeLabelLookupResult))
76        table
77        (branch
78          X86NativeLabelTableEmpty
79          .
80          (constructor X86NativeLabelLookupResult X86NativeLabelMissing))
81        (branch
82          X86NativeLabelTableEntry
83          existingName
84          offset
85          remaining
86          induction
87          .
88          (nat-eliminate
89            (lambda unrestricted equal : Nat . (family X86NativeLabelLookupResult))
90            induction
91            (lambda unrestricted predecessor : Nat .
92              (lambda unrestricted equalInduction : (family X86NativeLabelLookupResult) .
93                (constructor X86NativeLabelLookupResult X86NativeLabelFound offset)))
94            (bytes-equal name existingName))))))