From e989420b95f2c7c091bdb99459d87fdfdcd90898 Mon Sep 17 00:00:00 2001
From: John Tristan <jean.baptiste.tristan@gmail.com>
Date: Fri, 20 Sep 2024 11:08:51 -0400
Subject: [PATCH] fix namespace

---
 Main.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Main.lean b/Main.lean
index 24f5b26..58724d1 100644
--- a/Main.lean
+++ b/Main.lean
@@ -1,4 +1,4 @@
 import ANPU
 
 def main : IO Unit :=
-  IO.println s!"Hello, {hello}!"
+  IO.println s!"Hello, {ANPU.hello}!"