law length_take

bend-mathlib@0.8.1.0 · list.bend:277

import Base

277# Taking n elements leaves min(n, length) of them.
278law length_take:
279  for -a: Quant
280  for -A: Kind(a)
281  for xs: List<a, A>
282  for n: Nat
283  {List.length(a, A, List.take(a, A, xs, n)) == Nat.min(n, List.length(a, A, xs)) : Nat}