1037def lookupNameFrom :
1038 (pi unrestricted scope : (family NameScope) .
1039 (pi unrestricted identifier : Bytes . (pi unrestricted index : Nat . (family NameLookupResult)))) =
1040 (lambda unrestricted scope : (family NameScope) .
1041 (eliminate
1042 NameScope
1043 (lambda unrestricted value : (family NameScope) .
1044 (pi unrestricted identifier : Bytes .
1045 (pi unrestricted index : Nat . (family NameLookupResult))))
1046 scope
1047 (branch
1048 EmptyNameScope
1049 .
1050 (lambda unrestricted identifier : Bytes .
1051 (lambda unrestricted index : Nat . (constructor NameLookupResult NameNotFound identifier))))
1052 (branch
1053 NameScopeBinding
1054 bindingIdentifier
1055 outerScope
1056 ih_outerScope
1057 .
1058 (lambda unrestricted identifier : Bytes .
1059 (lambda unrestricted index : Nat .
1060 (app
1061 (nat-eliminate
1062 (lambda unrestricted condition : Nat .
1063 (pi unrestricted ignored : Nat . (family NameLookupResult)))
1064 (lambda unrestricted ignored : Nat . (ih_outerScope identifier (succ index)))
1065 (lambda unrestricted predecessor : Nat .
1066 (lambda unrestricted induction : (pi unrestricted ignored : Nat . (family NameLookupResult)) .
1067 (lambda unrestricted ignored : Nat .
1068 (constructor NameLookupResult NameFound index))))
1069 (coreBytesEqual bindingIdentifier identifier))
1070 zero))))))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.