Source/Packages

Compiler.DependentCore

packages/compiler/src/Compiler/DependentCore.alpha

12,943 lines498 declarations489.0 KiBSHA-256 ef207b0de796

def · lines 7382–7432

reduceCoreBytesEliminate

Full file
7382def reduceCoreBytesEliminate :
7383  (pi unrestricted motive : (family CoreTerm) .
7384    (pi unrestricted emptyCase : (family CoreTerm) .
7385      (pi unrestricted consCase : (family CoreTerm) .
7386        (pi unrestricted scrutinee : (family CoreTerm) . (family CoreTerm))))) =
7387  (lambda unrestricted motive : (family CoreTerm) .
7388    (lambda unrestricted emptyCase : (family CoreTerm) .
7389      (lambda unrestricted consCase : (family CoreTerm) .
7390        (lambda unrestricted scrutinee : (family CoreTerm) .
7391          (eliminate
7392            CoreLiteralInspection
7393            (lambda unrestricted inspection : (family CoreLiteralInspection) . (family CoreTerm))
7394            (inspectCoreLiteral scrutinee)
7395            (branch
7396              CoreNaturalInspected
7397              value
7398              .
7399              (corePrimitiveApplication4
7400                (constructor CorePrimitive CoreBytesEliminate)
7401                motive
7402                emptyCase
7403                consCase
7404                scrutinee))
7405            (branch
7406              CoreByteInspected
7407              value
7408              .
7409              (corePrimitiveApplication4
7410                (constructor CorePrimitive CoreBytesEliminate)
7411                motive
7412                emptyCase
7413                consCase
7414                scrutinee))
7415            (branch
7416              CoreBytesInspected
7417              value
7418              .
7419              (bytes-eliminate
7420                (lambda unrestricted remaining : Bytes . (family CoreTerm))
7421                emptyCase
7422                (reduceBytesEliminateStep consCase)
7423                value))
7424            (branch
7425              CoreNotLiteral
7426              .
7427              (corePrimitiveApplication4
7428                (constructor CorePrimitive CoreBytesEliminate)
7429                motive
7430                emptyCase
7431                consCase
7432                scrutinee)))))))

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.