AlphaGitHub
Source/Packages

Compiler.Codegen

packages/compiler/src/Compiler/Codegen.alpha

410 lines35 declarations12.1 KiBSHA-256 cd1660b56b4a
Download exact fileView at revisionf5034773ad4bb52133

def · lines 354–365

compileBytesValue

Full file
354def compileBytesValue =
355  (lambda unrestricted value : Bytes .
356    (nat-eliminate
357      (lambda unrestricted fits : Nat . (family CodegenResult))
358      (constructor
359        CodegenResult
360        CodegenUnsupportedTerm
361        (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))))))))
362      (lambda unrestricted predecessor : Nat .
363        (lambda unrestricted induction : (family CodegenResult) .
364          (constructor CodegenResult CodeGenerated (lowerBytesValue value))))
365      (nat-less-than (bytes-length value) (succ (bytes-length inlineByteCapacity128)))))

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.