Source/Packages

Compiler.DependentCore

packages/compiler/src/Compiler/DependentCore.alpha

12,943 lines498 declarations489.0 KiBSHA-256 ef207b0de796

def · lines 7060–7110

reduceCoreBytesCons

Full file
7060def reduceCoreBytesCons :
7061  (pi unrestricted left : (family CoreTerm) .
7062    (pi unrestricted right : (family CoreTerm) . (family CoreTerm))) =
7063  (lambda unrestricted left : (family CoreTerm) .
7064    (lambda unrestricted right : (family CoreTerm) .
7065      (eliminate
7066        CoreLiteralInspection
7067        (lambda unrestricted leftInspection : (family CoreLiteralInspection) . (family CoreTerm))
7068        (inspectCoreLiteral left)
7069        (branch
7070          CoreNaturalInspected
7071          value
7072          .
7073          (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesCons) left right))
7074        (branch
7075          CoreByteInspected
7076          leftValue
7077          .
7078          (eliminate
7079            CoreLiteralInspection
7080            (lambda unrestricted rightInspection : (family CoreLiteralInspection) .
7081              (family CoreTerm))
7082            (inspectCoreLiteral right)
7083            (branch
7084              CoreNaturalInspected
7085              value
7086              .
7087              (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesCons) left right))
7088            (branch
7089              CoreByteInspected
7090              value
7091              .
7092              (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesCons) left right))
7093            (branch
7094              CoreBytesInspected
7095              rightValue
7096              .
7097              (constructor CoreTerm CoreBytesLiteral (bytes-cons leftValue rightValue)))
7098            (branch
7099              CoreNotLiteral
7100              .
7101              (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesCons) left right))))
7102        (branch
7103          CoreBytesInspected
7104          value
7105          .
7106          (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesCons) left right))
7107        (branch
7108          CoreNotLiteral
7109          .
7110          (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesCons) 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.