The structural fold runs right-to-left. Consume exactly the adjacent numeric
token after Type; punctuation and following arguments stay in the tail.
5169def prependUniverseSequence =
5170 (lambda unrestricted head : (family Term) .
5171 (lambda unrestricted tail : (family TermList) .
5172 (eliminate
5173 TermList
5174 (lambda unrestricted value : (family TermList) . (family TermList))
5175 tail
5176 (branch TermListEnd . (constructor TermList TermListNext head tail))
5177 (branch
5178 TermListNext
5179 level
5180 remaining
5181 ih_remaining
5182 .
5183 (eliminate
5184 NaturalTermResult
5185 (lambda unrestricted value : (family NaturalTermResult) . (family TermList))
5186 (bareUniverseLevel level)
5187 (branch
5188 NaturalTermDecoded
5189 value
5190 .
5191 (constructor TermList TermListNext (constructor Term Universe value) remaining))
5192 (branch NotNaturalTerm . (constructor TermList TermListNext head tail)))))))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.