Source/Packages

Compiler.DependentCore

packages/compiler/src/Compiler/DependentCore.alpha

12,943 lines498 declarations489.0 KiBSHA-256 ef207b0de796

def · lines 7004–7058

reduceCoreBytesEqual

Full file
7004def reduceCoreBytesEqual :
7005  (pi unrestricted left : (family CoreTerm) .
7006    (pi unrestricted right : (family CoreTerm) . (family CoreTerm))) =
7007  (lambda unrestricted left : (family CoreTerm) .
7008    (lambda unrestricted right : (family CoreTerm) .
7009      (eliminate
7010        CoreLiteralInspection
7011        (lambda unrestricted leftInspection : (family CoreLiteralInspection) . (family CoreTerm))
7012        (inspectCoreLiteral left)
7013        (branch
7014          CoreNaturalInspected
7015          value
7016          .
7017          (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesEqual) left right))
7018        (branch
7019          CoreByteInspected
7020          value
7021          .
7022          (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesEqual) left right))
7023        (branch
7024          CoreBytesInspected
7025          leftValue
7026          .
7027          (eliminate
7028            CoreLiteralInspection
7029            (lambda unrestricted rightInspection : (family CoreLiteralInspection) .
7030              (family CoreTerm))
7031            (inspectCoreLiteral right)
7032            (branch
7033              CoreNaturalInspected
7034              value
7035              .
7036              (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesEqual) left right))
7037            (branch
7038              CoreByteInspected
7039              value
7040              .
7041              (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesEqual) left right))
7042            (branch
7043              CoreBytesInspected
7044              rightValue
7045              .
7046              (constructor
7047                CoreTerm
7048                CoreNaturalLiteral
7049                (Compiler.NaturalMagnitudeArithmetic/magnitudeFromNatural
7050                  (bytes-equal leftValue rightValue))))
7051            (branch
7052              CoreNotLiteral
7053              .
7054              (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesEqual) left right))))
7055        (branch
7056          CoreNotLiteral
7057          .
7058          (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesEqual) 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.