Answer helpers over the result family (the word type is explicit).
1142def stdDivisionQuotientOr =
1143 (lambda erased word : Type 0 .
1144 (lambda unrestricted fallback : word .
1145 (lambda unrestricted result : (family StdDivision word) .
1146 (eliminate
1147 StdDivision
1148 (lambda unrestricted current : (family StdDivision word) . word)
1149 result
1150 (branch StdDivisionSucceeded quotient remainder . quotient)
1151 (branch StdDivisionFailed error . fallback)))))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.