Source/Packages

Compiler.Elaborator

packages/compiler/src/Compiler/Elaborator.alpha

1,138 lines65 declarations36.4 KiBSHA-256 71619035ff76

def · lines 239–267

beginByteComparison

Full file
239def beginByteComparison =
240  (lambda unrestricted operation : Nat .
241    (lambda unrestricted left : (family ClosedNaturalElaboration) .
242      (eliminate
243        ClosedNaturalElaboration
244        (lambda unrestricted value : (family ClosedNaturalElaboration) .
245          (family ClosedNaturalElaboration))
246        left
247        (branch NaturalElaborated elaboratedNatural . unsupportedApplicationResult)
248        (branch BytesElaborated elaboratedBytes . unsupportedApplicationResult)
249        (branch
250          ByteElaborated
251          elaboratedByte
252          .
253          (constructor
254            ClosedNaturalElaboration
255            PrimitivePartial
256            (constructor PartialPrimitive PartialByteComparison operation elaboratedByte)))
257        (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
258        (branch
259          UnboundVariable
260          unboundSpelling
261          .
262          (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
263        (branch
264          UnsupportedTerm
265          unsupportedCode
266          .
267          (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode)))))

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.