708def checkBinderNameFresh :
709 (pi unrestricted candidate : Bytes .
710 (pi unrestricted scope : (family NameScope) .
711 (family FreshBinderNameResult))) =
712 (lambda unrestricted candidate : Bytes .
713 (lambda unrestricted scope : (family NameScope) .
714 (nat-eliminate
715 (lambda unrestricted candidateLength : Nat .
716 (family FreshBinderNameResult))
717 (constructor FreshBinderNameResult FreshBinderNameRejected
718 (constructor ApplicationBuilderError ApplicationBuilderEmptyBinderName)
719 zero)
720 (lambda unrestricted predecessor : Nat .
721 (lambda unrestricted induction : (family FreshBinderNameResult) .
722 (nat-eliminate
723 (lambda unrestricted collision : Nat .
724 (family FreshBinderNameResult))
725 (constructor FreshBinderNameResult FreshBinderNameBuilt
726 candidate (succ zero))
727 (lambda unrestricted ignoredPredecessor : Nat .
728 (lambda unrestricted ignoredInduction : (family FreshBinderNameResult) .
729 (constructor FreshBinderNameResult FreshBinderNameRejected
730 (constructor ApplicationBuilderError
731 ApplicationBuilderBinderFreshnessExhausted (succ zero))
732 (succ zero))))
733 (app
734 (app applicationBuilderScopeContains scope)
735 candidate))))
736 (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.