From a5ce6034de8ac6e852ab60dfccc6d1e82ba6bc16 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Tue, 23 Apr 2024 09:22:06 +0200
Subject: [PATCH] First test

---
 .gitignore           | 1 +
 nevanlinna/test.lean | 2 ++
 2 files changed, 3 insertions(+)

diff --git a/.gitignore b/.gitignore
index 20c60d7..37e9d24 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,2 +1,3 @@
 /build
 /lake-packages/*
+.lake
diff --git a/nevanlinna/test.lean b/nevanlinna/test.lean
index 8b13789..0849845 100644
--- a/nevanlinna/test.lean
+++ b/nevanlinna/test.lean
@@ -1 +1,3 @@
+import Mathlib.Topology.Basic
 
+#check TopologicalSpace