122def balancedInterval =
123 (lambda unrestricted extent : Nat .
124 (lambda unrestricted participants : Nat .
125 (lambda unrestricted role : Nat .
126 (nat-eliminate
127 (lambda unrestricted flag : Nat .
128 (family StdResult (family PartitionFailure) (family LogicalInterval)))
129 (constructor
130 StdResult
131 StdFailure
132 (family PartitionFailure)
133 (family LogicalInterval)
134 (constructor PartitionFailure PartitionExtentOutsideWord))
135 (lambda unrestricted predecessor : Nat .
136 (lambda unrestricted induction : (family StdResult (family PartitionFailure) (family LogicalInterval)) .
137 (nat-eliminate
138 (lambda unrestricted flag : Nat .
139 (family StdResult (family PartitionFailure) (family LogicalInterval)))
140 (constructor
141 StdResult
142 StdFailure
143 (family PartitionFailure)
144 (family LogicalInterval)
145 (constructor PartitionFailure PartitionNoParticipants))
146 (lambda unrestricted previous : Nat .
147 (lambda unrestricted rest : (family StdResult (family PartitionFailure) (family LogicalInterval)) .
148 (nat-eliminate
149 (lambda unrestricted flag : Nat .
150 (family StdResult (family PartitionFailure) (family LogicalInterval)))
151 (constructor
152 StdResult
153 StdFailure
154 (family PartitionFailure)
155 (family LogicalInterval)
156 (constructor PartitionFailure PartitionParticipantOutside))
157 (lambda unrestricted before : Nat .
158 (lambda unrestricted ignored : (family StdResult (family PartitionFailure) (family LogicalInterval)) .
159 (constructor
160 StdResult
161 StdSuccess
162 (family PartitionFailure)
163 (family LogicalInterval)
164 (balancedIntervalUnchecked extent participants role))))
165 (naturalLess role participants))))
166 (naturalNonzero participants))))
167 (naturalLessOrEqual extent 18446744073709551615)))))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.