AlphaGitHub
Source/Packages

Compiler.Elaborator

packages/compiler/src/Compiler/Elaborator.alpha

1,138 lines65 declarations36.4 KiBSHA-256 71619035ff76
Download exact fileView at revisionf5034773ad4bb52133

def · lines 300–327

beginNaturalLessThan

Full file
300def beginNaturalLessThan =
301  (lambda unrestricted left : (family ClosedNaturalElaboration) .
302    (eliminate
303      ClosedNaturalElaboration
304      (lambda unrestricted value : (family ClosedNaturalElaboration) .
305        (family ClosedNaturalElaboration))
306      left
307      (branch
308        NaturalElaborated
309        elaboratedNatural
310        .
311        (constructor
312          ClosedNaturalElaboration
313          PrimitivePartial
314          (constructor PartialPrimitive PartialNaturalLessThan elaboratedNatural)))
315      (branch BytesElaborated elaboratedBytes . unsupportedApplicationResult)
316      (branch ByteElaborated elaboratedByte . unsupportedApplicationResult)
317      (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
318      (branch
319        UnboundVariable
320        unboundSpelling
321        .
322        (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
323      (branch
324        UnsupportedTerm
325        unsupportedCode
326        .
327        (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.