Source/Packages

Compiler.Parser

packages/compiler/src/Compiler/Parser.alpha

5,902 lines337 declarations199.2 KiBSHA-256 6d135c41813d

def · lines 2023–2033

chooseDecodedAtom

Full file
2023def chooseDecodedAtom =
2024  (lambda unrestricted matched : Nat .
2025    (lambda unrestricted matchedTerm : (family Term) .
2026      (lambda unrestricted fallback : (family TermDecodeResult) .
2027        (nat-eliminate
2028          (lambda unrestricted value : Nat . (family TermDecodeResult))
2029          fallback
2030          (lambda unrestricted predecessor : Nat .
2031            (lambda unrestricted induction : (family TermDecodeResult) .
2032              (constructor TermDecodeResult TermDecoded matchedTerm)))
2033          matched))))

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.