125def naturalModulo =
126 (lambda unrestricted value : Nat .
127 (lambda unrestricted divisor : Nat .
128 (nat-eliminate
129 (lambda unrestricted current : Nat . (family NaturalModuloResult))
130 (constructor
131 NaturalModuloResult
132 NaturalModuloFailed
133 (constructor NaturalArithmeticErrorCode NaturalArithmeticModuloByZero))
134 (lambda unrestricted predecessor : Nat .
135 (lambda unrestricted induction : (family NaturalModuloResult) .
136 (constructor
137 NaturalModuloResult
138 NaturalModuloSucceeded
139 (naturalModuloUnchecked value divisor))))
140 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.