You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
import tactic
structureblah : Type :=
(f1 : ℕ)
(f2 : ℕ)
example : blah :=
begin
refine_struct {..},
case f1 {},
/-Invalid `case`: there is no goal tagged with suffix [f1].state:2 goalscase 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).
The text was updated successfully, but these errors were encountered:
Leaving this open for now since the tactic doc entry doesn't mention this (and the (text mode) tactic state says case), so there's still some potential for confusion here.
MWE:
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).
The text was updated successfully, but these errors were encountered: