chore: lake: tweak hovers for family_def et al

leanprover · May 7, 2024 · 9f63162 · 9f63162
1 parent 883a3e7
commit 9f63162
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 6 deletions.
diff --git a/src/lake/Lake/Build/Data.lean b/src/lake/Lake/Build/Data.lean
@@ -112,7 +112,7 @@ scoped macro (name := libraryDataDecl) doc?:optional(Parser.Command.docComment)
 "library_data " id:ident " : " ty:term : command => do
   let dty := mkCIdentFrom (← getRef) ``TargetData
   let key := Name.quoteFrom id id.getId
-  let id := mkIdentFrom id <| id.getId.modifyBase (`leanLib ++ ·)
+  let id := mkIdentFrom id (canonical := true) <| id.getId.modifyBase (`leanLib ++ ·)
   `($[$doc?]? family_def $id : $dty (`leanLib ++ $key) := $ty)
 
 /-- Macro for declaring new `TargetData`. -/

diff --git a/src/lake/Lake/Util/Family.lean b/src/lake/Lake/Util/Family.lean
@@ -171,7 +171,7 @@ scoped macro (name := familyDef) doc?:optional(Parser.Command.docComment)
   let tid := extractMacroScopes fam.getId |>.name
   if let (tid, _) :: _ ← Macro.resolveGlobalName tid then
     let app := Syntax.mkApp fam #[key]
-    let axm := mkIdentFrom fam <| `_root_ ++ tid ++ id.getId
+    let axm := mkIdentFrom id (canonical := true) <| `_root_ ++ tid ++ id.getId
     `($[$doc?]? @[simp] axiom $axm : $app = $ty
     instance : FamilyDef $fam $key $ty := ⟨$axm⟩)
   else

diff --git a/src/lake/Lake/Util/Name.lean b/src/lake/Lake/Util/Name.lean
@@ -90,7 +90,5 @@ instance : LawfulCmpEq Name Name.quickCmp where
 
 open Syntax
 
-def quoteFrom (ref : Syntax) : Name → Term
-| .anonymous => mkCIdentFrom ref ``anonymous
-| .str p s => mkApp (mkCIdentFrom ref ``mkStr) #[quoteFrom ref p, quote s]
-| .num p v => mkApp (mkCIdentFrom ref ``mkNum) #[quoteFrom ref p, quote v]
+def quoteFrom (ref : Syntax) (n : Name) : Term :=
+  ⟨copyHeadTailInfoFrom (quote n : Term) ref⟩