802def sm121LowerHas =
803 (lambda unrestricted registers : (family SM121LowerRegisters) .
804 (lambda unrestricted register : Nat .
805 (eliminate
806 SM121LowerRegisters
807 (lambda unrestricted current : (family SM121LowerRegisters) . Nat)
808 registers
809 (branch SM121LowerRegistersEnd . zero)
810 (branch SM121LowerRegistersNext head tail induction .
811 (nat-eliminate (lambda unrestricted current : Nat . Nat)
812 induction
813 (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat . (succ zero)))
814 (naturalEqual head register))))))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.