From dbdb06fb587de57a84f7b8a453b04706bc76a485 Mon Sep 17 00:00:00 2001 From: Andre Date: Fri, 16 Jun 2023 17:42:48 -0400 Subject: [PATCH] removed a comment --- CommAlg/final_poly_type.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean index e96aae3..dd35253 100644 --- a/CommAlg/final_poly_type.lean +++ b/CommAlg/final_poly_type.lean @@ -5,7 +5,6 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic set_option maxHeartbeats 0 macro "ls" : tactic => `(tactic|library_search) --- From Kyle : New tactic "obviously" -- From Kyle : New tactic "obviously" macro "obviously" : tactic => `(tactic| (