4308def decodeNonArithmeticVariableHead =
4309 (lambda unrestricted spelling : Bytes .
4310 (lambda unrestricted functionTerm : (family Term) .
4311 (lambda unrestricted argumentTerm : (family Term) .
4312 (lambda unrestricted remaining : (family TermList) .
4313 (chooseNamedDecode
4314 (bytesEqual spelling doSpelling)
4315 (lambda unrestricted force : Nat . (decodeDoApplication argumentTerm remaining))
4316 (lambda unrestricted force : Nat .
4317 (chooseNamedDecode
4318 (bytesEqual spelling letStarSpelling)
4319 (lambda unrestricted force : Nat .
4320 (decodeLocalLetSequence
4321 (constructor TermList TermListNext argumentTerm remaining)))
4322 (lambda unrestricted force : Nat .
4323 (chooseNamedDecode
4324 (bytesEqual spelling lambdaSpelling)
4325 (lambda unrestricted force : Nat .
4326 (decodeBinderForm zero argumentTerm remaining))
4327 (lambda unrestricted force : Nat .
4328 (chooseNamedDecode
4329 (bytesEqual spelling piSpelling)
4330 (lambda unrestricted force : Nat .
4331 (decodeBinderForm (succ zero) argumentTerm remaining))
4332 (lambda unrestricted force : Nat .
4333 (decodeNonBinderVariableHead spelling functionTerm argumentTerm remaining)))))))))))))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.