A bump allocator: the cursor after `count` items (each aligned to
`alignment` before it is taken), and the offset of item `index`.
108def cgBumpEnd =
109 (lambda unrestricted alignment : Nat .
110 (lambda unrestricted start : Nat .
111 (lambda unrestricted size : (pi unrestricted index : Nat . Nat) .
112 (lambda unrestricted count : Nat .
113 (app
114 (nat-eliminate
115 (lambda unrestricted current : Nat .
116 (pi unrestricted index : Nat . (pi unrestricted cursor : Nat . Nat)))
117 (lambda unrestricted index : Nat . (lambda unrestricted cursor : Nat . cursor))
118 (lambda unrestricted p : Nat .
119 (lambda unrestricted induction : (pi unrestricted index : Nat . (pi unrestricted cursor : Nat . Nat)) .
120 (lambda unrestricted index : Nat .
121 (lambda unrestricted cursor : Nat .
122 (induction (succ index) (naturalAdd (cgAlign cursor alignment) (size index)))))))
123 count)
124 0
125 start)))))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.