2228def decodeUniverseApplication =
2229 (lambda unrestricted levelTerm : (family Term) .
2230 (lambda unrestricted remaining : (family TermList) .
2231 (eliminate
2232 NaturalTermResult
2233 (lambda unrestricted value : (family NaturalTermResult) . (family TermDecodeResult))
2234 (naturalValueFromTerm levelTerm)
2235 (branch
2236 NaturalTermDecoded
2237 level
2238 .
2239 (requireNoMoreArguments (constructor Term Universe level) remaining))
2240 (branch
2241 NotNaturalTerm
2242 .
2243 (constructor
2244 TermDecodeResult
2245 TermDecodeFailed
2246 (succ (succ (succ (succ (succ (succ (succ (succ zero))))))))
2247 (constructor SyntaxOrigin SyntaxOriginUnknown))))))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.