AlphaGitHub
Source/Packages

Std.Word

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

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

def · lines 296–316

stdI8LessThan

Full file
signed order: if the signs differ the negative operand is less; if they agree the unsigned byte order IS the signed order.
296def stdI8LessThan =
297  (lambda unrestricted a : (family StdI8) .
298    (lambda unrestricted b : (family StdI8) .
299      (nat-eliminate
300        (lambda unrestricted current : Nat . Nat)
301        (nat-eliminate
302          (lambda unrestricted current : Nat . Nat)
303          (byte-less-than (stdI8ToByte a) (stdI8ToByte b))
304          (lambda unrestricted predecessor : Nat .
305            (lambda unrestricted induction : Nat . (succ zero)))
306          (stdI8IsNonNegative b))
307        (lambda unrestricted predecessor : Nat .
308          (lambda unrestricted induction : Nat .
309            (nat-eliminate
310              (lambda unrestricted current : Nat . Nat)
311              zero
312              (lambda unrestricted predecessorB : Nat .
313                (lambda unrestricted inductionB : Nat .
314                  (byte-less-than (stdI8ToByte a) (stdI8ToByte b))))
315              (stdI8IsNonNegative b))))
316        (stdI8IsNonNegative 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.