Compiler.MachineAArch64Assembly

88def aarch64LookupLabel :
89  (pi unrestricted name : Bytes .
90    (pi unrestricted labels : (family AArch64LabelTable) . (family AArch64LabelLookupResult))) =
91  (lambda unrestricted name : Bytes .
92    (lambda unrestricted labels : (family AArch64LabelTable) .
93      (eliminate
94        AArch64LabelTable
95        (lambda unrestricted current : (family AArch64LabelTable) .
96          (family AArch64LabelLookupResult))
97        labels
98        (branch AArch64LabelTableEmpty . (constructor AArch64LabelLookupResult AArch64LabelMissing))
99        (branch
100          AArch64LabelTableEntry
101          entryName
102          entryOffset
103          remaining
104          lookupRemaining
105          .
106          (nat-eliminate
107            (lambda unrestricted matches : Nat . (family AArch64LabelLookupResult))
108            lookupRemaining
109            (lambda unrestricted predecessor : Nat .
110              (lambda unrestricted induction : (family AArch64LabelLookupResult) .
111                (constructor AArch64LabelLookupResult AArch64LabelFound entryOffset)))
112            (bytes-equal entryName name))))))