37def learningRoundEqual =
38 (lambda unrestricted left : (family LearningRound) .
39 (lambda unrestricted right : (family LearningRound) .
40 (eliminate
41 LearningRound
42 (lambda unrestricted current : (family LearningRound) . Nat)
43 left
44 (branch
45 LearningRoundOf
46 leftEpoch
47 leftVersion
48 .
49 (eliminate
50 LearningRound
51 (lambda unrestricted current : (family LearningRound) . Nat)
52 right
53 (branch
54 LearningRoundOf
55 rightEpoch
56 rightVersion
57 .
58 (naturalAnd
59 (naturalEqual leftEpoch rightEpoch)
60 (naturalEqual leftVersion rightVersion))))))))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.