From 1a5d5f7b594a94d9514f7ad17c7d69aa2a447ada Mon Sep 17 00:00:00 2001 From: Greg Shuflin Date: Mon, 30 May 2022 19:03:42 -0700 Subject: [PATCH] Check directive --- gamarjoba.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/gamarjoba.lean b/gamarjoba.lean index 5e97341..51535c8 100644 --- a/gamarjoba.lean +++ b/gamarjoba.lean @@ -2,6 +2,7 @@ import system.io open io +#check (++) def greet (s : string) : io unit := put_str $ "Hello, " ++ s ++ "!\n"