SinTan1729/comm_alg
1
0
Fork 0
mirror of https://github.com/GTBarkley/comm_alg.git synced 2024-12-26 07:38:36 -06:00
Code Issues Projects Releases Packages Wiki Activity

removed a comment

Browse source
This commit is contained in:
Andre 2023-06-16 17:42:48 -04:00
parent dd45702fca
commit dbdb06fb58
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
CommAlg/final_poly_type.lean
View file

@ -5,7 +5,6 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
set_option maxHeartbeats 0 set_option maxHeartbeats 0
macro "ls" : tactic => `(tactic|library_search) macro "ls" : tactic => `(tactic|library_search)
-- From Kyle : New tactic "obviously"
-- From Kyle : New tactic "obviously" -- From Kyle : New tactic "obviously"
macro "obviously" : tactic => macro "obviously" : tactic =>
`(tactic| ( `(tactic| (