mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
21 lines
773 B
Lean4
21 lines
773 B
Lean4
def mkBig : Nat → String → String
|
|
| 0 s := s
|
|
| (k+1) s := mkBig k (s ++ "this is a big string\n")
|
|
|
|
def main : IO Unit :=
|
|
let s := mkBig 500000 "" in
|
|
let ss := s.split "\n" in
|
|
IO.println ss.length *>
|
|
IO.println (repr $ "aaa bbb ccc ddd".split) *>
|
|
IO.println (repr $ "aaa, bbb, ccc, ddd".split ", ") *>
|
|
IO.println (repr $ "aaa, bbb, ccc, ddd".split ",") *>
|
|
IO.println (repr $ "aaa,,,bbb,ccc,,ddd".split ",") *>
|
|
IO.println (repr $ "aaa#bbb#ccc#ddd".split "#") *>
|
|
IO.println (repr $ "aaa#bbb#ccc#ddd".split "") *>
|
|
IO.println (repr $ "aaa##bbb".split "##") *>
|
|
IO.println (repr $ "aaa##".split "##") *>
|
|
IO.println (repr $ "aaa#".split "#") *>
|
|
IO.println (repr $ "aaa".split "#") *>
|
|
IO.println (repr $ "aaa##bbb##".split "##") *>
|
|
IO.println (repr $ "aaa##bbb".split "##")
|