215def modelWord64IsZero =
216 (lambda unrestricted value : (family ModelWord64) .
217 (eliminate
218 ModelWord64
219 (lambda unrestricted current : (family ModelWord64) . Nat)
220 value
221 (branch
222 ModelWord64Value
223 b0
224 b1
225 b2
226 b3
227 b4
228 b5
229 b6
230 b7
231 .
232 (modelWord64FlagAnd
233 (byte-equal b0 (byte 0))
234 (modelWord64FlagAnd
235 (byte-equal b1 (byte 0))
236 (modelWord64FlagAnd
237 (byte-equal b2 (byte 0))
238 (modelWord64FlagAnd
239 (byte-equal b3 (byte 0))
240 (modelWord64FlagAnd
241 (byte-equal b4 (byte 0))
242 (modelWord64FlagAnd
243 (byte-equal b5 (byte 0))
244 (modelWord64FlagAnd (byte-equal b6 (byte 0)) (byte-equal b7 (byte 0))))))))))))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.