Inaccessible names can have characters following the dagger.

Author: Julian

lua/lean/infoview.lua

@@ -729,7 +729,7 @@ function Infoview:select_view_options()
     },
     {
       name = 'show inaccessible names',
-      description = 'Show inaccessible names (those ending in ✝)?',
+      description = 'Show inaccessible names (those containing ✝)?',
       option = 'show_hidden_assumptions',
     },
     {

lua/lean/widget/interactive_goal.lua

@@ -8,9 +8,13 @@ local lsp_diagnostics = require('lean.diagnostic').lsp_diagnostics
 local interactive_goal = {}
 
 ---A hypothesis name which is accessible according to Lean's naming conventions.
+---
+---Mirrors `Lean.Name.isInaccessibleUserName`: inaccessible names contain a
+---dagger anywhere within them, as shadowed names have further superscript
+---indices appended after theirs (e.g. `x✝¹`).
 ---@param name string
 local function is_accessible(name)
-  return name:sub(-#'✝') ~= '✝'
+  return not name:find('✝', 1, true)
 end
 
 ---Render a hypothesis name.

spec/infoview/view_options_spec.lua

@@ -51,6 +51,34 @@ describe('infoview view_options', function()
     )
   end)
 
+  it(
+    'can hide inaccessible names, even shadowed ones with indices',
+    helpers.clean_buffer(
+      [[
+        example : Nat → Nat → Nat → 37 = 37 := by
+          intro n n n
+          sorry
+      ]],
+      function()
+        helpers.search 'sorry'
+        assert.infoview_contents.are [[
+          n✝¹ n✝ n : Nat
+          ⊢ 37 = 37
+        ]]
+
+        local iv = infoview.get_current_infoview()
+        iv.view_options.show_hidden_assumptions = false
+        iv.pin:update()
+        assert.infoview_contents.are [[
+          n : Nat
+          ⊢ 37 = 37
+        ]]
+
+        iv.view_options.show_hidden_assumptions = true
+      end
+    )
+  )
+
   it(
     'can be selected interactively via <LocalLeader>v from a Lean buffer',
     helpers.clean_buffer(