151def dpotWhole =
152 (lambda unrestricted held : Nat .
153 (lambda unrestricted bytes : Nat .
154 (nat-eliminate
155 (lambda unrestricted current : Nat . (family StdList (family LogicalInterval)))
156 (constructor StdList StdListEmpty (family LogicalInterval))
157 (lambda unrestricted previous : Nat .
158 (lambda unrestricted ignored : (family StdList (family LogicalInterval)) .
159 (constructor
160 StdList
161 StdListCons
162 (family LogicalInterval)
163 (dpoInterval 0 bytes)
164 (constructor StdList StdListEmpty (family LogicalInterval)))))
165 held)))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.