law take_all

lawful-bytes@0.1.1.0 · proof_shift.bend:89

import Base

89law take_all:
90  for +ys: List<&2, U32>
91  for +n: Nat
92  for +h: {Nat.is_le(List.length(&2, U32, ys), n) == True{} : Bool}
93  {List.take(&2, U32, ys, n) == ys : List<&2, U32>}