3433def decodeDoStep =
3434 (lambda unrestricted term : (family Term) .
3435 (eliminate
3436 TermApplicationSpine
3437 (lambda unrestricted value : (family TermApplicationSpine) . (family DoStepDecodeResult))
3438 (termApplicationSpine term)
3439 (branch
3440 TermApplicationSpineValue
3441 head
3442 arguments
3443 .
3444 (eliminate
3445 TermSpellingResult
3446 (lambda unrestricted result : (family TermSpellingResult) . (family DoStepDecodeResult))
3447 (termSpelling head)
3448 (branch
3449 TermSpellingDecoded
3450 headSpelling
3451 .
3452 (chooseDecodedDoStep
3453 term
3454 (eliminate
3455 QuantityDecodeResult
3456 (lambda unrestricted result : (family QuantityDecodeResult) .
3457 (family DoStepDecodeResult))
3458 (decodeQuantitySpelling headSpelling)
3459 (branch QuantityDecoded quantity . (decodeDoLongNamed quantity arguments))
3460 (branch
3461 QuantityInvalid
3462 .
3463 (decodeDoNamedTail (succ (succ (succ zero))) headSpelling arguments)))))
3464 (branch
3465 TermHasNoSpelling
3466 .
3467 (constructor
3468 DoStepDecodeResult
3469 DoStepDecoded
3470 zero
3471 (succ (succ (succ zero)))
3472 b""
3473 term))))))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.