leanprover-community / batteries

The "batteries included" extended library for the Lean programming language and theorem prover
Apache License 2.0
254 stars 107 forks source link

rcases doesn't seem to support ?_ placeholders #116

Open Ruben-VandeVelde opened 1 year ago

Ruben-VandeVelde commented 1 year ago
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'"

alreadydone commented 1 year ago

Currently my workaround is

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

which is kind of annoying.