53def regionTransferIdentityEqual =
54 (lambda unrestricted expected : (family RegionTransferIdentity) .
55 (lambda unrestricted actual : (family RegionTransferIdentity) .
56 (eliminate
57 RegionTransferIdentity
58 (lambda unrestricted current : (family RegionTransferIdentity) . Nat)
59 expected
60 (branch
61 RegionTransferIdentityOf
62 expectedComposition
63 expectedRun
64 expectedRegion
65 expectedRepresentation
66 expectedRound
67 expectedOperation
68 expectedSender
69 expectedReceiver
70 expectedInterval
71 .
72 (eliminate
73 RegionTransferIdentity
74 (lambda unrestricted current : (family RegionTransferIdentity) . Nat)
75 actual
76 (branch
77 RegionTransferIdentityOf
78 actualComposition
79 actualRun
80 actualRegion
81 actualRepresentation
82 actualRound
83 actualOperation
84 actualSender
85 actualReceiver
86 actualInterval
87 .
88 (naturalAnd
89 (bytes-equal expectedComposition actualComposition)
90 (naturalAnd
91 (bytes-equal expectedRun actualRun)
92 (naturalAnd
93 (bytes-equal expectedRegion actualRegion)
94 (naturalAnd
95 (bytes-equal expectedRepresentation actualRepresentation)
96 (naturalAnd
97 (learningRoundEqual expectedRound actualRound)
98 (naturalAnd
99 (naturalEqual expectedOperation actualOperation)
100 (naturalAnd
101 (naturalEqual expectedSender actualSender)
102 (naturalAnd
103 (naturalEqual expectedReceiver actualReceiver)
104 (naturalAnd
105 (naturalEqual
106 (intervalBegin expectedInterval)
107 (intervalBegin actualInterval))
108 (naturalEqual
109 (intervalEnd expectedInterval)
110 (intervalEnd actualInterval)))))))))))))))))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.