Source/Packages

Compiler.DependentCore

packages/compiler/src/Compiler/DependentCore.alpha

12,943 lines498 declarations489.0 KiBSHA-256 ef207b0de796

def · lines 6784–6838

reduceCoreByteEqual

Full file
6784def reduceCoreByteEqual :
6785  (pi unrestricted left : (family CoreTerm) .
6786    (pi unrestricted right : (family CoreTerm) . (family CoreTerm))) =
6787  (lambda unrestricted left : (family CoreTerm) .
6788    (lambda unrestricted right : (family CoreTerm) .
6789      (eliminate
6790        CoreLiteralInspection
6791        (lambda unrestricted leftInspection : (family CoreLiteralInspection) . (family CoreTerm))
6792        (inspectCoreLiteral left)
6793        (branch
6794          CoreNaturalInspected
6795          value
6796          .
6797          (corePrimitiveApplication2 (constructor CorePrimitive CoreByteEqual) left right))
6798        (branch
6799          CoreByteInspected
6800          leftValue
6801          .
6802          (eliminate
6803            CoreLiteralInspection
6804            (lambda unrestricted rightInspection : (family CoreLiteralInspection) .
6805              (family CoreTerm))
6806            (inspectCoreLiteral right)
6807            (branch
6808              CoreNaturalInspected
6809              value
6810              .
6811              (corePrimitiveApplication2 (constructor CorePrimitive CoreByteEqual) left right))
6812            (branch
6813              CoreByteInspected
6814              rightValue
6815              .
6816              (constructor
6817                CoreTerm
6818                CoreNaturalLiteral
6819                (Compiler.NaturalMagnitudeArithmetic/magnitudeFromNatural
6820                  (byte-equal leftValue rightValue))))
6821            (branch
6822              CoreBytesInspected
6823              value
6824              .
6825              (corePrimitiveApplication2 (constructor CorePrimitive CoreByteEqual) left right))
6826            (branch
6827              CoreNotLiteral
6828              .
6829              (corePrimitiveApplication2 (constructor CorePrimitive CoreByteEqual) left right))))
6830        (branch
6831          CoreBytesInspected
6832          value
6833          .
6834          (corePrimitiveApplication2 (constructor CorePrimitive CoreByteEqual) left right))
6835        (branch
6836          CoreNotLiteral
6837          .
6838          (corePrimitiveApplication2 (constructor CorePrimitive CoreByteEqual) 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.