686def freshBinderName :
687 (pi unrestricted candidate : Bytes .
688 (pi unrestricted scope : (family NameScope) .
689 (family FreshBinderNameResult))) =
690 (lambda unrestricted candidate : Bytes .
691 (lambda unrestricted scope : (family NameScope) .
692 (nat-eliminate
693 (lambda unrestricted candidateLength : Nat .
694 (family FreshBinderNameResult))
695 (constructor FreshBinderNameResult FreshBinderNameRejected
696 (constructor ApplicationBuilderError ApplicationBuilderEmptyBinderName)
697 zero)
698 (lambda unrestricted predecessor : Nat .
699 (lambda unrestricted induction : (family FreshBinderNameResult) .
700 (app
701 (app
702 (app applicationBuilderFreshBinderSearch
703 (succ (app applicationBuilderScopeDepth scope)))
704 candidate)
705 scope)))
706 (bytes-length candidate))))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.