law length_take_sym

bend-mathlib@0.8.1.0 · string.bend:682

import Base

682# Taking n characters leaves min(n, length) of them, reversed to rewrite toward the simple side.
683law length_take_sym:
684  for s: String
685  for n: Nat
686  {Nat.min(n, String.length(s)) == String.length(String.take(s, n)) : Nat}