From 076d9b8bfa9909390ec73cb435089801c17ae8e0 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 12 Apr 2024 09:39:17 +0200 Subject: [PATCH] change main file --- BonnAnalysis.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/BonnAnalysis.lean b/BonnAnalysis.lean index e99d3a6..3fe12e7 100644 --- a/BonnAnalysis.lean +++ b/BonnAnalysis.lean @@ -1 +1,2 @@ -def hello := "world" \ No newline at end of file +-- When adding a new file, import it in this file +import BonnAnalysis.Plancherel