Strings

Strings in Lean

Strings in Lean are written with double quotes. You can concatenate them with ++:

#eval "Hello" ++ ", World!"   -- "Hello, World!"

Note: #eval on a String shows it with quotes (that is Lean's display format for strings). Use IO.println to print without quotes.

You can get the length of a string using .length:

#eval "Lean".length    -- 4

Your Turn

1. Concatenate "Lean " and "is fun" and evaluate it
2. Evaluate the length of "functional"