def gt.hl_elist

bend-osdev-gf@0.1.1.0 · proof_tab.bend:253

import Base
import bend-osdev-array@0.1.0.1/array.bend as A
import bend-osdev-gf@0.1.1.0/gf.bend as G

253def gt.hl_elist(+f: G.Gf8Field) -> {List.length(&2, U32, gt.elist(510n, f, 0n)) == A.Arrays.slots(9n) : Nat}:
254  {==}