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