From 1be737b4de4c5c189a159ff4aef0e334f90f238a Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 7 Feb 2025 13:49:10 +0000
Subject: [PATCH] feat: Remove declarations from lean snippets

---
 HepLean/Meta/Basic.lean         | 16 +++++++++++++++-
 scripts/MetaPrograms/notes.lean |  2 +-
 2 files changed, 16 insertions(+), 2 deletions(-)

diff --git a/HepLean/Meta/Basic.lean b/HepLean/Meta/Basic.lean
index 3fc53fd..5f3f93a 100644
--- a/HepLean/Meta/Basic.lean
+++ b/HepLean/Meta/Basic.lean
@@ -128,7 +128,7 @@ def getDocString (c : Name) : CoreM String := do
   let doc? ← findDocString? env c
   return doc?.getD ""
 
-/-- Given a name, returns the source code defining that name. -/
+/-- Given a name, returns the source code defining that name, including doc strings. -/
 def getDeclString (name : Name) : CoreM String := do
   let env ← getEnv
   match ← findDeclarationRanges? name with
@@ -141,6 +141,20 @@ def getDeclString (name : Name) : CoreM String := do
     | none => return ""
   | none => return ""
 
+/-- Given a name, returns the source code defining that name,
+  starting with the def ... or lemma...  etc. -/
+def getDeclStringNoDoc (name : Name) : CoreM String := do
+  let declerationString ← getDeclString name
+  let headerLine (line : String) : Bool :=
+    line.startsWith "def " ∨ line.startsWith "lemma " ∨ line.startsWith "inductive "
+    ∨ line.startsWith "structure " ∨ line.startsWith "theorem "
+    ∨ line.startsWith "instance " ∨ line.startsWith "abbrev " ∨
+    line.startsWith "noncomputable def "
+  let lines := declerationString.splitOn "\n"
+  match lines.findIdx? headerLine with
+  | none => panic! s!"{name} has no header line"
+  | some i => return String.intercalate "\n" (lines.drop i)
+
 end Lean.Name
 
 namespace HepLean
diff --git a/scripts/MetaPrograms/notes.lean b/scripts/MetaPrograms/notes.lean
index f794474..f54ae88 100644
--- a/scripts/MetaPrograms/notes.lean
+++ b/scripts/MetaPrograms/notes.lean
@@ -44,7 +44,7 @@ structure DeclInfo where
 def DeclInfo.ofName (n : Name) (ns : NameStatus): MetaM DeclInfo := do
   let line ← Name.lineNumber n
   let fileName ← Name.fileName n
-  let declString ← Name.getDeclString n
+  let declString ← Name.getDeclStringNoDoc n
   let docString ← Name.getDocString n
   let constInfo ← getConstInfo n
   let isDef := constInfo.isDef ∨ Lean.isStructure (← getEnv) n ∨ constInfo.isInductive