law length_zip

bend-mathlib@0.8.1.0 · list.bend:430

import Base

430# A zip is as long as the shorter of the two lists.
431law length_zip:
432  for -a: Quant
433  for -A: Kind(a)
434  for xs: List<a, A>
435  for ys: List<a, A>
436  {List.length(&1, A & A, List.zip(a, A, a, A, xs, ys)) == Nat.min(List.length(a, A, xs), List.length(a, A, ys)) : Nat}