AlphaGitHub
Source/Packages

Std.Word

packages/foundation/standard/src/Std/Word.alpha

1,783 lines192 declarations64.2 KiBSHA-256 27bf8c3f30ee
Download exact fileView at revisionf5034773ad4bb52133

def · lines 237–256

stdI64LessThan

Full file
I64 SIGNED comparison (two's complement, L11h). If the sign bits differ the negative operand is less; if they agree, the unsigned order IS the signed order. Returns the Nat flag ((succ zero) = less). Distinct from stdU64LessThan (NUM-004: signed vs unsigned comparisons are distinct).
237def stdI64LessThan =
238  (lambda unrestricted a : (family StdI64) .
239    (lambda unrestricted b : (family StdI64) .
240      (nat-eliminate
241        (lambda unrestricted current : Nat . Nat)
242        (nat-eliminate
243          (lambda unrestricted current : Nat . Nat)
244          (modelWord64LessThan (stdI64ToWord a) (stdI64ToWord b))
245          (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
246          (modelWord64HighBit (stdI64ToWord b)))
247        (lambda unrestricted predecessor : Nat .
248          (lambda unrestricted induction : Nat .
249            (nat-eliminate
250              (lambda unrestricted current : Nat . Nat)
251              (succ zero)
252              (lambda unrestricted predecessorB : Nat .
253                (lambda unrestricted inductionB : Nat .
254                  (modelWord64LessThan (stdI64ToWord a) (stdI64ToWord b))))
255              (modelWord64HighBit (stdI64ToWord b)))))
256        (modelWord64HighBit (stdI64ToWord a)))))

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.