feat: deriving instances: use accessible names (#10271)

This PR changes the naming of the internal functions in deriving
instances like BEq to use accessible names. This is necessary to
reasonably easily prove things about these functions. For example after
`deriving BEq` for a type `T`, the implementation of `instBEqT` is in
`instBEqT.beq`.

src/Lean/CoreM.lean

@@ -353,7 +353,7 @@ def instantiateValueLevelParams (c : ConstantInfo) (us : List Level) : CoreM Exp
     if us == us' then
       return r
   unless c.hasValue do
-    throwError "Not a definition or theorem: {c.name}"
+    throwError "Not a definition or theorem: {.ofConstName c.name}"
   let r := c.instantiateValueLevelParams! us
   modifyInstLevelValueCache fun s => s.insert c.name (us, r)
   return r

src/Lean/Elab/Deriving/BEq.lean

@@ -119,7 +119,7 @@ def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
     end)
 
 private def mkBEqInstanceCmds (declName : Name) : TermElabM (Array Syntax) := do
-  let ctx ← mkContext "beq" declName
+  let ctx ← mkContext ``BEq "beq" declName
   let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `BEq #[declName])
   trace[Elab.Deriving.beq] "\n{cmds}"
   return cmds
@@ -129,7 +129,7 @@ private def mkBEqEnumFun (ctx : Context) (name : Name) : TermElabM Syntax := do
   `(def $(mkIdent auxFunName):ident  (x y : $(mkCIdent name)) : Bool := x.ctorIdx == y.ctorIdx)
 
 private def mkBEqEnumCmd (name : Name): TermElabM (Array Syntax) := do
-  let ctx ← mkContext "beq" name
+  let ctx ← mkContext ``BEq "beq" name
   let cmds := #[← mkBEqEnumFun ctx name] ++ (← mkInstanceCmds ctx `BEq #[name])
   trace[Elab.Deriving.beq] "\n{cmds}"
   return cmds

src/Lean/Elab/Deriving/DecEq.lean

@@ -194,7 +194,7 @@ def mkAuxFunctions (ctx : Context) : TermElabM (TSyntax `command) := do
   `(command| mutual $[$res:command]* end)
 
 def mkDecEqCmds (indVal : InductiveVal) : TermElabM (Array Syntax) := do
-  let ctx ← mkContext "decEq" indVal.name
+  let ctx ← mkContext ``DecidableEq "decEq" indVal.name
   let cmds := #[← mkAuxFunctions ctx] ++ (← mkInstanceCmds ctx `DecidableEq #[indVal.name] (useAnonCtor := false))
   trace[Elab.Deriving.decEq] "\n{cmds}"
   return cmds

src/Lean/Elab/Deriving/FromToJson.lean

@@ -215,13 +215,13 @@ def mkFromJsonMutualBlock (ctx : Context) : TermElabM Command := do
     end)
 
 private def mkToJsonInstance (declName : Name) : TermElabM (Array Command) := do
-  let ctx ← mkContext "toJson" declName
+  let ctx ← mkContext ``ToJson "toJson" declName
   let cmds := #[← mkToJsonMutualBlock ctx] ++ (← mkInstanceCmds ctx ``ToJson #[declName])
   trace[Elab.Deriving.toJson] "\n{cmds}"
   return cmds
 
 private def mkFromJsonInstance (declName : Name) : TermElabM (Array Command) := do
-  let ctx ← mkContext "fromJson" declName
+  let ctx ← mkContext ``FromJson "fromJson" declName
   let cmds := #[← mkFromJsonMutualBlock ctx] ++ (← mkInstanceCmds ctx ``FromJson #[declName])
   trace[Elab.Deriving.fromJson] "\n{cmds}"
   return cmds

src/Lean/Elab/Deriving/Hashable.lean

@@ -81,7 +81,7 @@ def mkHashFuncs (ctx : Context) : TermElabM Syntax := do
   `(mutual $auxDefs:command* end)
 
 private def mkHashableInstanceCmds (declName : Name) : TermElabM (Array Syntax) := do
-  let ctx ← mkContext "hash" declName
+  let ctx ← mkContext ``Hashable "hash" declName
   let cmds := #[← mkHashFuncs ctx] ++ (← mkInstanceCmds ctx `Hashable #[declName])
   trace[Elab.Deriving.hashable] "\n{cmds}"
   return cmds

src/Lean/Elab/Deriving/Inhabited.lean

@@ -61,7 +61,7 @@ where
   /-- Create an `instance` command using the constructor `ctorName` with a hypothesis `Inhabited α` when `α` is one of the inductive type parameters
      at position `i` and `i ∈ assumingParamIdxs`. -/
   mkInstanceCmdWith (assumingParamIdxs : IndexSet) : TermElabM Syntax := do
-    let ctx ← Deriving.mkContext "inhabited" inductiveTypeName
+    let ctx ← Deriving.mkContext ``Inhabited "inhabited" inductiveTypeName
     let indVal ← getConstInfoInduct inductiveTypeName
     let ctorVal ← getConstInfoCtor ctorName
     let mut indArgs := #[]
@@ -81,7 +81,7 @@ where
     for _ in *...ctorVal.numFields do
       ctorArgs := ctorArgs.push (← ``(Inhabited.default))
     let val ← `(@$(mkIdent ctorName):ident $ctorArgs*)
-    let ctx ← mkContext "default" inductiveTypeName
+    let ctx ← mkContext ``Inhabited "default" inductiveTypeName
     let auxFunName := ctx.auxFunNames[0]!
     `(def $(mkIdent auxFunName):ident $binders:bracketedBinder* : $type := $val
       instance $binders:bracketedBinder* : Inhabited $type := ⟨$(mkIdent auxFunName)⟩)

src/Lean/Elab/Deriving/Ord.lean

@@ -90,7 +90,7 @@ def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
     end)
 
 private def mkOrdInstanceCmds (declName : Name) : TermElabM (Array Syntax) := do
-  let ctx ← mkContext "ord" declName
+  let ctx ← mkContext ``Ord "ord" declName
   let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `Ord #[declName])
   trace[Elab.Deriving.ord] "\n{cmds}"
   return cmds

src/Lean/Elab/Deriving/Repr.lean

@@ -114,7 +114,7 @@ def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
     end)
 
 private def mkReprInstanceCmd (declName : Name) : TermElabM (Array Syntax) := do
-  let ctx ← mkContext "repr" declName
+  let ctx ← mkContext ``Repr "repr" declName
   let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `Repr #[declName])
   trace[Elab.Deriving.repr] "\n{cmds}"
   return cmds

src/Lean/Elab/Deriving/ToExpr.lean

@@ -216,7 +216,7 @@ def mkInstanceCmds (ctx : Deriving.Context) (typeNames : Array Name) :
 Returns all the commands necessary to construct the `ToExpr` instances.
 -/
 def mkToExprInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax) := do
-  let ctx ← mkContext "toExpr" declNames[0]!
+  let ctx ← mkContext ``ToExpr "toExpr" declNames[0]!
   let cmds := #[← mkAuxFunctions ctx] ++ (← mkInstanceCmds ctx declNames)
   trace[Elab.Deriving.toExpr] "\n{cmds}"
   return cmds

src/Lean/Elab/Deriving/Util.lean

@@ -9,6 +9,7 @@ prelude
 public import Lean.Elab.Term
 public import Lean.Elab.Command
 meta import Lean.Parser.Command
+import Lean.Elab.DeclNameGen
 
 public section
 
@@ -84,23 +85,33 @@ def withoutExposeFromCtors (typeName : Name) (cont : CommandElabM α) : CommandE
   else cont
 
 structure Context where
+  instName    : Name
   typeInfos   : Array InductiveVal
   auxFunNames : Array Name
   usePartial  : Bool
 
-def mkContext (fnPrefix : String) (typeName : Name) : TermElabM Context := do
+
+def mkContext (className : Name) (fnPrefix : String) (typeName : Name) : TermElabM Context := do
   let indVal ← getConstInfoInduct typeName
   let mut typeInfos := #[]
   for typeName in indVal.all do
     typeInfos := typeInfos.push (← getConstInfoInduct typeName)
+  let instName ← do -- anticipate the instance name
+    let argNames     ← mkInductArgNames indVal
+    let binders      ← mkImplicitBinders argNames
+    let indType      ← mkInductiveApp indVal argNames
+    let type         ← `($(mkCIdent className) $indType)
+    NameGen.mkBaseNameWithSuffix' "inst" (binders.map (·.raw)) type
   let mut auxFunNames := #[]
-  for typeName in indVal.all do
-    match typeName.eraseMacroScopes with
-    | .str _ t => auxFunNames := auxFunNames.push (← mkFreshUserName <| Name.mkSimple <| fnPrefix ++ t)
-    | _        => auxFunNames := auxFunNames.push (← mkFreshUserName `instFn)
-  trace[Elab.Deriving.beq] "{auxFunNames}"
+  if indVal.all.length = 1 then
+    auxFunNames := auxFunNames.push (instName ++ .mkSimple fnPrefix)
+  else
+    for i in [:indVal.all.length] do
+      auxFunNames := auxFunNames.push (instName ++ .mkSimple s!"{fnPrefix}_{i+1}")
+  trace[Elab.Deriving] "instName: {instName} auxFunNames: {auxFunNames}"
   let usePartial := indVal.isNested || typeInfos.size > 1
   return {
+    instName    := instName
     typeInfos   := typeInfos
     auxFunNames := auxFunNames
     usePartial  := usePartial
@@ -143,7 +154,7 @@ def mkInstanceCmds (ctx : Context) (className : Name) (typeNames : Array Name) (
       let mut val      := mkIdent auxFunName
       if useAnonCtor then
         val ← `(⟨$val⟩)
-      let instCmd ← `(instance $binders:implicitBinder* : $type := $val)
+      let instCmd ← `(instance $(mkIdent ctx.instName):ident $binders:implicitBinder* : $type := $val)
       instances := instances.push instCmd
   return instances
 

tests/lean/decEqMutualInductives.lean.expected.out

@@ -1,108 +1,108 @@
 [Elab.Deriving.decEq] 
     [mutual
-       def decEqTree✝ (x✝ : @A.Tree✝) (x✝¹ : @A.Tree✝) : Decidable✝ (x✝ = x✝¹) :=
+       def instDecidableEqListTree.decEq_1 (x✝ : @A.Tree✝) (x✝¹ : @A.Tree✝) : Decidable✝ (x✝ = x✝¹) :=
          match x✝, x✝¹ with
          | @A.Tree.node a✝, @A.Tree.node b✝ =>
-           let inst✝ := decEqListTree✝ @a✝ @b✝;
+           let inst✝ := instDecidableEqListTree.decEq_2 @a✝ @b✝;
            if h✝ : @a✝ = @b✝ then by subst h✝; exact isTrue✝ rfl✝
            else isFalse✝ (by intro n✝; injection n✝; apply h✝ _; assumption)
        termination_by structural x✝
-       def decEqListTree✝ (x✝² : @A.ListTree✝) (x✝³ : @A.ListTree✝) : Decidable✝ (x✝² = x✝³) :=
+       def instDecidableEqListTree.decEq_2 (x✝² : @A.ListTree✝) (x✝³ : @A.ListTree✝) : Decidable✝ (x✝² = x✝³) :=
          match x✝², x✝³ with
          | @A.ListTree.nil, @A.ListTree.nil => isTrue✝¹ rfl✝¹
          | A.ListTree.nil .., A.ListTree.cons .. => isFalse✝¹ (by intro h✝¹; injection h✝¹)
          | A.ListTree.cons .., A.ListTree.nil .. => isFalse✝¹ (by intro h✝¹; injection h✝¹)
          | @A.ListTree.cons a✝¹ a✝², @A.ListTree.cons b✝¹ b✝² =>
-           let inst✝¹ := decEqTree✝ @a✝¹ @b✝¹;
+           let inst✝¹ := instDecidableEqListTree.decEq_1 @a✝¹ @b✝¹;
            if h✝² : @a✝¹ = @b✝¹ then by subst h✝²;
              exact
-               let inst✝² := decEqListTree✝ @a✝² @b✝²;
+               let inst✝² := instDecidableEqListTree.decEq_2 @a✝² @b✝²;
                if h✝³ : @a✝² = @b✝² then by subst h✝³; exact isTrue✝² rfl✝²
                else isFalse✝² (by intro n✝¹; injection n✝¹; apply h✝³ _; assumption)
            else isFalse✝³ (by intro n✝²; injection n✝²; apply h✝² _; assumption)
        termination_by structural x✝²
      end,
-     instance : DecidableEq✝ (@A.ListTree✝) :=
-       decEqListTree✝]
+     instance instDecidableEqListTree : DecidableEq✝ (@A.ListTree✝) :=
+       instDecidableEqListTree.decEq_2]
 [Elab.Deriving.decEq] 
     [mutual
-       def decEqFoo₁✝ (x✝ : @A.Foo₁✝) (x✝¹ : @A.Foo₁✝) : Decidable✝ (x✝ = x✝¹) :=
+       def instDecidableEqFoo₁.decEq_1 (x✝ : @A.Foo₁✝) (x✝¹ : @A.Foo₁✝) : Decidable✝ (x✝ = x✝¹) :=
          match x✝, x✝¹ with
          | @A.Foo₁.foo₁₁, @A.Foo₁.foo₁₁ => isTrue✝ rfl✝
          | A.Foo₁.foo₁₁ .., A.Foo₁.foo₁₂ .. => isFalse✝ (by intro h✝; injection h✝)
          | A.Foo₁.foo₁₂ .., A.Foo₁.foo₁₁ .. => isFalse✝ (by intro h✝; injection h✝)
          | @A.Foo₁.foo₁₂ a✝, @A.Foo₁.foo₁₂ b✝ =>
-           let inst✝ := decEqFoo₂✝ @a✝ @b✝;
+           let inst✝ := instDecidableEqFoo₁.decEq_2 @a✝ @b✝;
            if h✝¹ : @a✝ = @b✝ then by subst h✝¹; exact isTrue✝¹ rfl✝¹
            else isFalse✝¹ (by intro n✝; injection n✝; apply h✝¹ _; assumption)
        termination_by structural x✝
-       def decEqFoo₂✝ (x✝² : @A.Foo₂✝) (x✝³ : @A.Foo₂✝) : Decidable✝ (x✝² = x✝³) :=
+       def instDecidableEqFoo₁.decEq_2 (x✝² : @A.Foo₂✝) (x✝³ : @A.Foo₂✝) : Decidable✝ (x✝² = x✝³) :=
          match x✝², x✝³ with
          | @A.Foo₂.foo₂ a✝¹, @A.Foo₂.foo₂ b✝¹ =>
-           let inst✝¹ := decEqFoo₃✝ @a✝¹ @b✝¹;
+           let inst✝¹ := instDecidableEqFoo₁.decEq_3 @a✝¹ @b✝¹;
            if h✝² : @a✝¹ = @b✝¹ then by subst h✝²; exact isTrue✝² rfl✝²
            else isFalse✝² (by intro n✝¹; injection n✝¹; apply h✝² _; assumption)
        termination_by structural x✝²
-       def decEqFoo₃✝ (x✝⁴ : @A.Foo₃✝) (x✝⁵ : @A.Foo₃✝) : Decidable✝ (x✝⁴ = x✝⁵) :=
+       def instDecidableEqFoo₁.decEq_3 (x✝⁴ : @A.Foo₃✝) (x✝⁵ : @A.Foo₃✝) : Decidable✝ (x✝⁴ = x✝⁵) :=
          match x✝⁴, x✝⁵ with
          | @A.Foo₃.foo₃ a✝², @A.Foo₃.foo₃ b✝² =>
-           let inst✝² := decEqFoo₁✝ @a✝² @b✝²;
+           let inst✝² := instDecidableEqFoo₁.decEq_1 @a✝² @b✝²;
            if h✝³ : @a✝² = @b✝² then by subst h✝³; exact isTrue✝³ rfl✝³
            else isFalse✝³ (by intro n✝²; injection n✝²; apply h✝³ _; assumption)
        termination_by structural x✝⁴
      end,
-     instance : DecidableEq✝ (@A.Foo₁✝) :=
-       decEqFoo₁✝]
+     instance instDecidableEqFoo₁ : DecidableEq✝ (@A.Foo₁✝) :=
+       instDecidableEqFoo₁.decEq_1]
 [Elab.Deriving.decEq] 
     [mutual
-       def decEqTree✝ (x✝ : @B.Tree✝) (x✝¹ : @B.Tree✝) : Decidable✝ (x✝ = x✝¹) :=
+       def instDecidableEqListTree.decEq_1 (x✝ : @B.Tree✝) (x✝¹ : @B.Tree✝) : Decidable✝ (x✝ = x✝¹) :=
          B.Tree.match_on_same_ctor✝ x✝ x✝¹ rfl✝
            @fun a✝ b✝ =>
-             let inst✝ := decEqListTree✝ @a✝ @b✝;
+             let inst✝ := instDecidableEqListTree.decEq_2 @a✝ @b✝;
              if h✝ : @a✝ = @b✝ then by subst h✝; exact isTrue✝ rfl✝¹
              else isFalse✝ (by intro n✝; injection n✝; apply h✝ _; assumption)
        termination_by structural x✝
-       def decEqListTree✝ (x✝² : @B.ListTree✝) (x✝³ : @B.ListTree✝) : Decidable✝ (x✝² = x✝³) :=
+       def instDecidableEqListTree.decEq_2 (x✝² : @B.ListTree✝) (x✝³ : @B.ListTree✝) : Decidable✝ (x✝² = x✝³) :=
          if h✝¹ : B.ListTree.ctorIdx✝ x✝² = B.ListTree.ctorIdx✝ x✝³ then
            B.ListTree.match_on_same_ctor✝ x✝² x✝³ h✝¹ (@fun => isTrue✝¹ rfl✝)
              @fun a✝¹ a✝² b✝¹ b✝² =>
-               let inst✝¹ := decEqTree✝ @a✝¹ @b✝¹;
+               let inst✝¹ := instDecidableEqListTree.decEq_1 @a✝¹ @b✝¹;
                if h✝² : @a✝¹ = @b✝¹ then by subst h✝²;
                  exact
-                   let inst✝² := decEqListTree✝ @a✝² @b✝²;
+                   let inst✝² := instDecidableEqListTree.decEq_2 @a✝² @b✝²;
                    if h✝³ : @a✝² = @b✝² then by subst h✝³; exact isTrue✝² rfl✝²
                    else isFalse✝¹ (by intro n✝¹; injection n✝¹; apply h✝³ _; assumption)
                else isFalse✝² (by intro n✝²; injection n✝²; apply h✝² _; assumption)
          else isFalse✝³ (fun h'✝ => h✝¹ (congrArg✝ B.ListTree.ctorIdx✝ h'✝))
        termination_by structural x✝²
      end,
-     instance : DecidableEq✝ (@B.ListTree✝) :=
-       decEqListTree✝]
+     instance instDecidableEqListTree : DecidableEq✝ (@B.ListTree✝) :=
+       instDecidableEqListTree.decEq_2]
 [Elab.Deriving.decEq] 
     [mutual
-       def decEqFoo₁✝ (x✝ : @B.Foo₁✝) (x✝¹ : @B.Foo₁✝) : Decidable✝ (x✝ = x✝¹) :=
+       def instDecidableEqFoo₁.decEq_1 (x✝ : @B.Foo₁✝) (x✝¹ : @B.Foo₁✝) : Decidable✝ (x✝ = x✝¹) :=
          if h✝ : B.Foo₁.ctorIdx✝ x✝ = B.Foo₁.ctorIdx✝ x✝¹ then
            B.Foo₁.match_on_same_ctor✝ x✝ x✝¹ h✝ (@fun => isTrue✝ rfl✝)
              @fun a✝ b✝ =>
-               let inst✝ := decEqFoo₂✝ @a✝ @b✝;
+               let inst✝ := instDecidableEqFoo₁.decEq_2 @a✝ @b✝;
                if h✝¹ : @a✝ = @b✝ then by subst h✝¹; exact isTrue✝¹ rfl✝¹
                else isFalse✝ (by intro n✝; injection n✝; apply h✝¹ _; assumption)
          else isFalse✝¹ (fun h'✝ => h✝ (congrArg✝ B.Foo₁.ctorIdx✝ h'✝))
        termination_by structural x✝
-       def decEqFoo₂✝ (x✝² : @B.Foo₂✝) (x✝³ : @B.Foo₂✝) : Decidable✝ (x✝² = x✝³) :=
+       def instDecidableEqFoo₁.decEq_2 (x✝² : @B.Foo₂✝) (x✝³ : @B.Foo₂✝) : Decidable✝ (x✝² = x✝³) :=
          B.Foo₂.match_on_same_ctor✝ x✝² x✝³ rfl✝
            @fun a✝¹ b✝¹ =>
-             let inst✝¹ := decEqFoo₃✝ @a✝¹ @b✝¹;
+             let inst✝¹ := instDecidableEqFoo₁.decEq_3 @a✝¹ @b✝¹;
              if h✝² : @a✝¹ = @b✝¹ then by subst h✝²; exact isTrue✝² rfl✝²
              else isFalse✝² (by intro n✝¹; injection n✝¹; apply h✝² _; assumption)
        termination_by structural x✝²
-       def decEqFoo₃✝ (x✝⁴ : @B.Foo₃✝) (x✝⁵ : @B.Foo₃✝) : Decidable✝ (x✝⁴ = x✝⁵) :=
+       def instDecidableEqFoo₁.decEq_3 (x✝⁴ : @B.Foo₃✝) (x✝⁵ : @B.Foo₃✝) : Decidable✝ (x✝⁴ = x✝⁵) :=
          B.Foo₃.match_on_same_ctor✝ x✝⁴ x✝⁵ rfl✝
            @fun a✝² b✝² =>
-             let inst✝² := decEqFoo₁✝ @a✝² @b✝²;
+             let inst✝² := instDecidableEqFoo₁.decEq_1 @a✝² @b✝²;
              if h✝³ : @a✝² = @b✝² then by subst h✝³; exact isTrue✝³ rfl✝³
              else isFalse✝³ (by intro n✝²; injection n✝²; apply h✝³ _; assumption)
        termination_by structural x✝⁴
      end,
-     instance : DecidableEq✝ (@B.Foo₁✝) :=
-       decEqFoo₁✝]
+     instance instDecidableEqFoo₁ : DecidableEq✝ (@B.Foo₁✝) :=
+       instDecidableEqFoo₁.decEq_1]

tests/lean/prvNameWithMacroScopes.lean

@@ -1,2 +0,0 @@
-import Lean
-#print Lean.instBEqFVarId

tests/lean/prvNameWithMacroScopes.lean.expected.out

@@ -1,2 +0,0 @@
-def Lean.instBEqFVarId : BEq Lean.FVarId :=
-{ beq := Lean.beqFVarId✝ }

tests/lean/run/2161.lean

@@ -19,7 +19,7 @@ because its `Decidable` instance
   instDecidableEqFoo (((mul 4 1).mul 1).mul 1) 4
 did not reduce to `isTrue` or `isFalse`.
 
-After unfolding the instances `decEqFoo✝`, `instDecidableEqFoo`, `instDecidableEqNat`, and `Nat.decEq`, reduction got stuck at the `Decidable` instance
+After unfolding the instances `instDecidableEqFoo`, `instDecidableEqNat`, `Nat.decEq`, and `instDecidableEqFoo.decEq`, reduction got stuck at the `Decidable` instance
   match h : (((mul 4 1).mul 1).mul 1).num.beq 4 with
   | true => isTrue ⋯
   | false => isFalse ⋯
@@ -39,7 +39,7 @@ because its `Decidable` instance
   instDecidableEqFoo (((add 4 1).add 1).add 1) 4
 did not reduce to `isTrue` or `isFalse`.
 
-After unfolding the instances `decEqFoo✝`, `instDecidableEqFoo`, `instDecidableEqNat`, and `Nat.decEq`, reduction got stuck at the `Decidable` instance
+After unfolding the instances `instDecidableEqFoo`, `instDecidableEqNat`, `Nat.decEq`, and `instDecidableEqFoo.decEq`, reduction got stuck at the `Decidable` instance
   match h : (((add 4 1).add 1).add 1).num.beq 4 with
   | true => isTrue ⋯
   | false => isFalse ⋯

tests/lean/run/decEq.lean

@@ -32,7 +32,9 @@ public inductive PubInd where
   | a (n : Nat) | b
 deriving DecidableEq
 
-/-- info: Decidable.rec (fun h => false) (fun h => true) (decEqPubInd✝ PubInd.b PubInd.b) -/
+/--
+info: Decidable.rec (fun h => false) (fun h => true) (instDecidableEqPubInd.decEq PubInd.b PubInd.b)
+-/
 #guard_msgs in
 #with_exporting
 #reduce decide (PubInd.b = PubInd.b)

tests/lean/run/derivingBEq.lean

@@ -75,7 +75,7 @@ structure PrivField where
   private a : Nat
 deriving BEq
 
-/-- info: fun a => beqPrivField✝ a a -/
+/-- info: fun a => instBEqPrivField.beq a a -/
 #guard_msgs in
 #with_exporting
 #reduce fun (a : PrivField) => a == a
@@ -88,7 +88,7 @@ public structure PrivField2 where
   private a : Nat
 deriving BEq
 
-/-- info: fun a => beqPrivField2✝ a a -/
+/-- info: fun a => instBEqPrivField2.beq a a -/
 #guard_msgs in
 #with_exporting
 #reduce fun (a : PrivField2) => a == a

tests/lean/run/derivingInhabited.lean

@@ -55,7 +55,7 @@ deriving Inhabited
 
 /--
 info: private def instInhabitedA : Inhabited A :=
-{ default := defaultA✝ }
+{ default := instInhabitedA.default }
 -/
 #guard_msgs in
 #print instInhabitedA
@@ -66,7 +66,7 @@ public structure PrivField where
   private a : Nat
 deriving Inhabited
 
-/-- info: defaultPrivField✝ -/
+/-- info: instInhabitedPrivField.default -/
 #guard_msgs in
 #with_exporting
 #reduce (default : PrivField)

tests/lean/run/derivingRepr.lean

@@ -122,7 +122,7 @@ structure PrivField where
   private a : Nat
 deriving Repr
 
-/-- info: fun a => reprPrivField✝ a 0 -/
+/-- info: fun a => instReprPrivField.repr a 0 -/
 #guard_msgs in
 #with_exporting
 #reduce fun (a : PrivField) => repr a
@@ -135,7 +135,7 @@ public structure PrivField2 where
   private a : Nat
 deriving Repr
 
-/-- info: fun a => reprPrivField2✝ a 0 -/
+/-- info: fun a => instReprPrivField2.repr a 0 -/
 #guard_msgs in
 #with_exporting
 #reduce fun (a : PrivField2) => repr a
@@ -147,7 +147,7 @@ deriving Repr
 
 /--
 info: @[expose] def instReprPublic : Repr Public :=
-{ reprPrec := reprPublic✝ }
+{ reprPrec := instReprPublic.repr }
 -/
 #guard_msgs in
 #with_exporting

tests/lean/run/prvNameWithMacroScopes.lean

@@ -0,0 +1,13 @@
+macro "test%" n:ident : command =>
+  `(def foo := 42
+    def $n := foo
+  )
+
+test% bar
+
+/--
+info: def bar : Nat :=
+foo✝
+-/
+#guard_msgs in
+#print bar