A term-returning reducer never manufactures an inadmissible literal.
Checked inference and erasure expose the explicit rejection separately.
2903def reduceCoreArithmetic =
2904 (lambda unrestricted operation : (family CoreNaturalOperation) .
2905 (lambda unrestricted left : (family CoreTerm) .
2906 (lambda unrestricted right : (family CoreTerm) .
2907 (eliminate
2908 CoreArithmeticInspection
2909 (lambda unrestricted result : (family CoreArithmeticInspection) . (family CoreTerm))
2910 (inspectCoreArithmetic operation left right)
2911 (branch CoreArithmeticValue digits . (constructor CoreTerm CoreNaturalLiteral digits))
2912 (branch
2913 CoreArithmeticNeutral
2914 .
2915 (constructor CoreTerm CoreNaturalArithmetic operation left right))
2916 (branch
2917 CoreArithmeticRejected
2918 failure
2919 .
2920 (constructor CoreTerm CoreNaturalArithmetic operation 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.