11207def lookupTypeWithShift :
11208 (pi unrestricted context : (family TypeContext) .
11209 (pi unrestricted index : Nat .
11210 (pi unrestricted amount : Nat .
11211 (pi unrestricted originalIndex : Nat . (family TypeLookupResult))))) =
11212 (lambda unrestricted context : (family TypeContext) .
11213 (eliminate
11214 TypeContext
11215 (lambda unrestricted value : (family TypeContext) .
11216 (pi unrestricted index : Nat .
11217 (pi unrestricted amount : Nat .
11218 (pi unrestricted originalIndex : Nat . (family TypeLookupResult)))))
11219 context
11220 (branch
11221 EmptyTypeContext
11222 .
11223 (lambda unrestricted index : Nat .
11224 (lambda unrestricted amount : Nat .
11225 (lambda unrestricted originalIndex : Nat .
11226 (constructor TypeLookupResult TypeNotFound originalIndex)))))
11227 (branch
11228 TypeContextBinding
11229 bindingType
11230 outerContext
11231 ih_outerContext
11232 .
11233 (lambda unrestricted index : Nat .
11234 (lambda unrestricted amount : Nat .
11235 (lambda unrestricted originalIndex : Nat .
11236 (app
11237 (nat-eliminate
11238 (lambda unrestricted value : Nat .
11239 (pi unrestricted ignored : Nat . (family TypeLookupResult)))
11240 (lambda unrestricted ignored : Nat .
11241 (constructor TypeLookupResult TypeFound (shiftCoreBy amount bindingType)))
11242 (lambda unrestricted predecessor : Nat .
11243 (lambda unrestricted induction : (pi unrestricted ignored : Nat . (family TypeLookupResult)) .
11244 (lambda unrestricted ignored : Nat .
11245 (ih_outerContext predecessor (succ amount) originalIndex))))
11246 index)
11247 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.