law length_take

bend-mathlib@0.8.1.0 · string.bend:446

import Base

446# Taking n characters leaves min(n, length) of them.
447law length_take:
448  for s: String
449  for n: Nat
450  {String.length(String.take(s, n)) == Nat.min(n, String.length(s)) : Nat}