String.lean « Common - aoc-2023 - Advent of Code 2023 - I'm still learning Lean4, so please don't judge.

summary refs log tree commit diff

path: root/Common/String.lean

blob: 7fe7aeef5790415f5f056e0cdb53e8b5952a319b (plain) (blame)

namespace String

def splitTrim (c : Char → Bool) (s : String) : List String :=
  String.trim <$> s.split c