mathlib

mathlib copied to clipboard

MWE:

import tactic

structure blah : Type :=
(f1 : ℕ)
(f2 : ℕ)

example : blah :=
begin
  refine_struct {..},
  case f1 {},
  /-
Invalid `case`: there is no goal tagged with suffix [f1].
state:
2 goals
case blah, f1
⊢ ℕ

case blah, f2
⊢ ℕ
-/
end

Also, the case tags don't show up in the widget view of the tactic state in VS Code (they still show up if I switch to the plain text view).