142def naturalDivisionStep =
143 (lambda unrestricted divisor : Nat .
144 (lambda unrestricted state : (family NaturalDivisionState) .
145 (eliminate
146 NaturalDivisionState
147 (lambda unrestricted current : (family NaturalDivisionState) .
148 (family NaturalDivisionState))
149 state
150 (branch
151 NaturalDivisionStateValue
152 remainder
153 quotient
154 .
155 (app
156 (lambda unrestricted incremented : Nat .
157 (nat-eliminate
158 (lambda unrestricted condition : Nat . (family NaturalDivisionState))
159 (constructor NaturalDivisionState NaturalDivisionStateValue incremented quotient)
160 (lambda unrestricted predecessor : Nat .
161 (lambda unrestricted induction : (family NaturalDivisionState) .
162 (constructor
163 NaturalDivisionState
164 NaturalDivisionStateValue
165 zero
166 (succ quotient))))
167 (naturalEqual incremented divisor)))
168 (succ remainder))))))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.