batteries icon indicating copy to clipboard operation
batteries copied to clipboard

rcases doesn't seem to support ?_ placeholders

Open Ruben-VandeVelde opened this issue 1 year ago • 1 comments

import Std.Tactic.RCases

theorem aux (h : 0 < 2) : ∃ n : Nat, n = 2 := ⟨2, rfl⟩

example : True := by
  rcases aux ?_ with ⟨x, h⟩
  trivial

I would expect a side goal to be created (like in lean3), but get "don't know how to synthesize placeholder for argument 'h'"

Ruben-VandeVelde avatar Apr 16 '23 20:04 Ruben-VandeVelde

Currently my workaround is

have := aux ?_
rcases this with ⟨x, h⟩

which is kind of annoying.

alreadydone avatar Aug 27 '23 07:08 alreadydone