---- the parameters (bytes from the video arena's base) ----
entry 0 the embedding (vocabulary x width); entry 1 + 9 l + k layer l's
k-th item (ln1 gamma, ln1 beta, qkv, o, ln2 gamma, ln2 beta, up, gate,
down); entries 145, 146 the final gamma and beta
the offsets of items 0 .. count - 1, computed in one pass (the plan
looks them up for every launch)
140def cgBumpTable =
141 (lambda unrestricted alignment : Nat .
142 (lambda unrestricted start : Nat .
143 (lambda unrestricted size : (pi unrestricted index : Nat . Nat) .
144 (lambda unrestricted count : Nat .
145 (app
146 (nat-eliminate
147 (lambda unrestricted current : Nat .
148 (pi unrestricted index : Nat .
149 (pi unrestricted cursor : Nat . (family StdList Nat))))
150 (lambda unrestricted index : Nat .
151 (lambda unrestricted cursor : Nat . (constructor StdList StdListEmpty Nat)))
152 (lambda unrestricted p : Nat .
153 (lambda unrestricted induction : (pi unrestricted index : Nat . (pi unrestricted cursor : Nat . (family StdList Nat))) .
154 (lambda unrestricted index : Nat .
155 (lambda unrestricted cursor : Nat .
156 (let unrestricted offset =
157 (cgAlign cursor alignment)
158 in
159 (constructor
160 StdList
161 StdListCons
162 Nat
163 offset
164 (induction (succ index) (naturalAdd offset (size index)))))))))
165 count)
166 0
167 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.