185def naturalDivide =
186 (lambda unrestricted value : Nat .
187 (lambda unrestricted divisor : Nat .
188 (nat-eliminate
189 (lambda unrestricted current : Nat . (family NaturalDivideResult))
190 (constructor
191 NaturalDivideResult
192 NaturalDivideFailed
193 (constructor NaturalArithmeticErrorCode NaturalArithmeticDivideByZero))
194 (lambda unrestricted predecessor : Nat .
195 (lambda unrestricted induction : (family NaturalDivideResult) .
196 (constructor
197 NaturalDivideResult
198 NaturalDivideSucceeded
199 (naturalDivideUnchecked value divisor))))
200 divisor)))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.