From ec88f8065b8f9d065bc05162b4ecf71b158cfefe Mon Sep 17 00:00:00 2001 From: Antonio De Lucreziis Date: Fri, 29 Sep 2023 13:55:16 +0200 Subject: [PATCH] ehm fix --- Main.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Main.lean b/Main.lean index 8551474..fedff09 100644 --- a/Main.lean +++ b/Main.lean @@ -1,6 +1,6 @@ import Prova def main : IO Unit := - IO.println "Hello, {hello}!" + IO.println s!"Hello, {hello}!" #eval main