law list_len_take

bend-osdev-mode-core@0.1.0.0 · LAWS.bend:62

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B

62law list_len_take:
63  for +n: Nat
64  for +xs: List<&2, U32>
65  for h1: {Nat.is_le(n, B.len(xs)) == True{} : Bool}
66  {B.len(B.take(n, xs)) == n : Nat}