Source/Packages

Compiler.Elaborator

packages/compiler/src/Compiler/Elaborator.alpha

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

def · lines 480–487

chooseNaturalLessApplication

Full file
480def chooseNaturalLessApplication =
481  (lambda unrestricted spelling : Bytes .
482    (lambda unrestricted argument : (family ClosedNaturalElaboration) .
483      (selectPrimitiveBySpelling
484        spelling
485        naturalLessThanSpelling
486        (beginNaturalLessThan argument)
487        (chooseBytesConsApplication spelling argument))))

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.