def gt.hl_rep

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

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

250def gt.hl_rep(+d: Nat) -> {List.length(&2, U32, List.replicate(U32, A.Arrays.slots(d), 0)) == A.Arrays.slots(d) : Nat}:
251  gt.rep_len(A.Arrays.slots(d))