From 5bbb84f5f1eb52e30d6c67fa60dc4577e4f3ee05 Mon Sep 17 00:00:00 2001 From: poincare-duality Date: Fri, 9 Jun 2023 17:40:22 -0700 Subject: [PATCH] Give it a try --- CommAlg.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/CommAlg.lean b/CommAlg.lean index e99d3a6..cef13f8 100644 --- a/CommAlg.lean +++ b/CommAlg.lean @@ -1 +1,4 @@ -def hello := "world" \ No newline at end of file +import Mathlib.Tactic +def hello := "world" + +-- Thank Grant for setting this up. \ No newline at end of file