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.