---- 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)
139def cgBumpTable =
140 (lambda unrestricted alignment : Nat .
141 (lambda unrestricted start : Nat .
142 (lambda unrestricted size : (pi unrestricted index : Nat . Nat) .
143 (lambda unrestricted count : Nat .
144 (app
145 (nat-eliminate
146 (lambda unrestricted current : Nat .
147 (pi unrestricted index : Nat .
148 (pi unrestricted cursor : Nat . (family StdList Nat))))
149 (lambda unrestricted index : Nat .
150 (lambda unrestricted cursor : Nat . (constructor StdList StdListEmpty Nat)))
151 (lambda unrestricted p : Nat .
152 (lambda unrestricted induction : (pi unrestricted index : Nat . (pi unrestricted cursor : Nat . (family StdList Nat))) .
153 (lambda unrestricted index : Nat .
154 (lambda unrestricted cursor : Nat .
155 (let unrestricted offset =
156 (cgAlign cursor alignment)
157 in
158 (constructor
159 StdList
160 StdListCons
161 Nat
162 offset
163 (induction (succ index) (naturalAdd offset (size index)))))))))
164 count)
165 0
166 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.