6896def reduceCoreNaturalLess :
6897 (pi unrestricted left : (family CoreTerm) .
6898 (pi unrestricted right : (family CoreTerm) . (family CoreTerm))) =
6899 (lambda unrestricted left : (family CoreTerm) .
6900 (lambda unrestricted right : (family CoreTerm) .
6901 (eliminate
6902 CoreLiteralInspection
6903 (lambda unrestricted leftInspection : (family CoreLiteralInspection) . (family CoreTerm))
6904 (inspectCoreLiteral left)
6905 (branch
6906 CoreNaturalInspected
6907 leftValue
6908 .
6909 (eliminate
6910 CoreLiteralInspection
6911 (lambda unrestricted rightInspection : (family CoreLiteralInspection) .
6912 (family CoreTerm))
6913 (inspectCoreLiteral right)
6914 (branch
6915 CoreNaturalInspected
6916 rightValue
6917 .
6918 (constructor
6919 CoreTerm
6920 CoreNaturalLiteral
6921 (Compiler.NaturalMagnitudeArithmetic/magnitudeFromNatural
6922 (Compiler.NaturalMagnitudeArithmetic/magnitudeLess leftValue rightValue))))
6923 (branch
6924 CoreByteInspected
6925 value
6926 .
6927 (corePrimitiveApplication2 (constructor CorePrimitive CoreNaturalLess) left right))
6928 (branch
6929 CoreBytesInspected
6930 value
6931 .
6932 (corePrimitiveApplication2 (constructor CorePrimitive CoreNaturalLess) left right))
6933 (branch
6934 CoreNotLiteral
6935 .
6936 (corePrimitiveApplication2 (constructor CorePrimitive CoreNaturalLess) left right))))
6937 (branch
6938 CoreByteInspected
6939 value
6940 .
6941 (corePrimitiveApplication2 (constructor CorePrimitive CoreNaturalLess) left right))
6942 (branch
6943 CoreBytesInspected
6944 value
6945 .
6946 (corePrimitiveApplication2 (constructor CorePrimitive CoreNaturalLess) left right))
6947 (branch
6948 CoreNotLiteral
6949 .
6950 (corePrimitiveApplication2 (constructor CorePrimitive CoreNaturalLess) 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.