law is_empty_iff_length_eq_zero

bend-mathlib@0.8.1.0 · string.bend:386

import Base

386# A string is empty exactly when its length is zero.
387law is_empty_iff_length_eq_zero:
388  for s: String
389  {String.is_empty(s) == Nat.is_eq(String.length(s), 0n) : Bool}