126def transferRequirePhase =
127 (lambda unrestricted expected : Nat .
128 (lambda unrestricted next : (family TransferPhase) .
129 (lambda unrestricted actual : (family TransferPhase) .
130 (nat-eliminate
131 (lambda unrestricted flag : Nat .
132 (family StdResult (family TransferFailure) (family TransferPhase)))
133 (constructor
134 StdResult
135 StdFailure
136 (family TransferFailure)
137 (family TransferPhase)
138 (constructor TransferFailure TransferIllegalPhase))
139 (lambda unrestricted previous : Nat .
140 (lambda unrestricted ignored : (family StdResult (family TransferFailure) (family TransferPhase)) .
141 (constructor
142 StdResult
143 StdSuccess
144 (family TransferFailure)
145 (family TransferPhase)
146 next)))
147 (naturalEqual expected (transferPhaseCode actual))))))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.