Post History
Lean 4, 39 bytes def x(i:String):String:=s!"Hello, {i}!" Try it online! (Note that TIO only supports Lean 3, so I sadly am unable to use a link from there.)
#1: Initial revision
by
CrSb0001
·
2025-04-10T20:00:03Z (9 days ago)
# Lean 4, 39 bytes
```lean
def x(i:String):String:=s!"Hello, {i}!"
```
[Try it online!](https://live.lean-lang.org/#codez=CYUwZgBAHgFAlgLgMoBcBOcB2BzAlM9LbBAXgGcBCAIgAkQAbegewBoIBvOAX2oCheAxCABuAQ3rQIVAMJokAIwAMygIxUgA) (Note that TIO only supports Lean 3, so I sadly am unable to use a link from there.)