6840def reduceCoreByteLess :
6841 (pi unrestricted left : (family CoreTerm) .
6842 (pi unrestricted right : (family CoreTerm) . (family CoreTerm))) =
6843 (lambda unrestricted left : (family CoreTerm) .
6844 (lambda unrestricted right : (family CoreTerm) .
6845 (eliminate
6846 CoreLiteralInspection
6847 (lambda unrestricted leftInspection : (family CoreLiteralInspection) . (family CoreTerm))
6848 (inspectCoreLiteral left)
6849 (branch
6850 CoreNaturalInspected
6851 value
6852 .
6853 (corePrimitiveApplication2 (constructor CorePrimitive CoreByteLess) left right))
6854 (branch
6855 CoreByteInspected
6856 leftValue
6857 .
6858 (eliminate
6859 CoreLiteralInspection
6860 (lambda unrestricted rightInspection : (family CoreLiteralInspection) .
6861 (family CoreTerm))
6862 (inspectCoreLiteral right)
6863 (branch
6864 CoreNaturalInspected
6865 value
6866 .
6867 (corePrimitiveApplication2 (constructor CorePrimitive CoreByteLess) left right))
6868 (branch
6869 CoreByteInspected
6870 rightValue
6871 .
6872 (constructor
6873 CoreTerm
6874 CoreNaturalLiteral
6875 (Compiler.NaturalMagnitudeArithmetic/magnitudeFromNatural
6876 (byte-less-than leftValue rightValue))))
6877 (branch
6878 CoreBytesInspected
6879 value
6880 .
6881 (corePrimitiveApplication2 (constructor CorePrimitive CoreByteLess) left right))
6882 (branch
6883 CoreNotLiteral
6884 .
6885 (corePrimitiveApplication2 (constructor CorePrimitive CoreByteLess) left right))))
6886 (branch
6887 CoreBytesInspected
6888 value
6889 .
6890 (corePrimitiveApplication2 (constructor CorePrimitive CoreByteLess) left right))
6891 (branch
6892 CoreNotLiteral
6893 .
6894 (corePrimitiveApplication2 (constructor CorePrimitive CoreByteLess) left right)))))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.