601def applicationBuilderScopeDepth :
602 (pi unrestricted scope : (family NameScope) . Nat) =
603 (lambda unrestricted scope : (family NameScope) .
604 (eliminate NameScope
605 (lambda unrestricted value : (family NameScope) . Nat)
606 scope
607 (branch EmptyNameScope . zero)
608 (branch NameScopeBinding identifier outer induction .
609 (succ induction))))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.