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 567–586

stdI16LessThan

Full file
567def stdI16LessThan =
568  (lambda unrestricted a : (family StdI16) .
569    (lambda unrestricted b : (family StdI16) .
570      (nat-eliminate
571        (lambda unrestricted current : Nat . Nat)
572        (nat-eliminate
573          (lambda unrestricted current : Nat . Nat)
574          (stdU16LessThan (stdI16ToU16 a) (stdI16ToU16 b))
575          (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
576          (stdU16HighBit (stdI16ToU16 b)))
577        (lambda unrestricted predecessor : Nat .
578          (lambda unrestricted induction : Nat .
579            (nat-eliminate
580              (lambda unrestricted current : Nat . Nat)
581              (succ zero)
582              (lambda unrestricted predecessorB : Nat .
583                (lambda unrestricted inductionB : Nat .
584                  (stdU16LessThan (stdI16ToU16 a) (stdI16ToU16 b))))
585              (stdU16HighBit (stdI16ToU16 b)))))
586        (stdU16HighBit (stdI16ToU16 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.