645def applicationBuilderFreshBinderSearch :
646 (pi unrestricted fuel : Nat .
647 (pi unrestricted candidate : Bytes .
648 (pi unrestricted scope : (family NameScope) .
649 (family FreshBinderNameResult)))) =
650 (lambda unrestricted fuel : Nat .
651 (nat-eliminate
652 (lambda unrestricted remainingFuel : Nat .
653 (pi unrestricted candidate : Bytes .
654 (pi unrestricted scope : (family NameScope) .
655 (family FreshBinderNameResult))))
656 (lambda unrestricted candidate : Bytes .
657 (lambda unrestricted scope : (family NameScope) .
658 (constructor FreshBinderNameResult FreshBinderNameRejected
659 (constructor ApplicationBuilderError
660 ApplicationBuilderBinderFreshnessExhausted zero)
661 zero)))
662 (lambda unrestricted predecessor : Nat .
663 (lambda unrestricted induction :
664 (pi unrestricted candidate : Bytes .
665 (pi unrestricted scope : (family NameScope) .
666 (family FreshBinderNameResult))) .
667 (lambda unrestricted candidate : Bytes .
668 (lambda unrestricted scope : (family NameScope) .
669 (nat-eliminate
670 (lambda unrestricted collision : Nat .
671 (family FreshBinderNameResult))
672 (constructor FreshBinderNameResult FreshBinderNameBuilt
673 candidate (succ zero))
674 (lambda unrestricted ignoredPredecessor : Nat .
675 (lambda unrestricted ignoredInduction : (family FreshBinderNameResult) .
676 (app applicationBuilderIncrementFreshResult
677 (app
678 (app induction
679 (bytes-append candidate b"'"))
680 scope))))
681 (app
682 (app applicationBuilderScopeContains scope)
683 candidate))))))
684 fuel))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.