Zulip Chat Archive
Stream: general
Topic: exact and new goals
Reid Barton (Nov 26 2018 at 15:00):
How come exact
makes _
s appearing inside record constructors into new goals?
structure C := (x : ℕ) example : C := by exact ⟨_⟩ -- error on _, "don't know how to synthesize placeholder" example : C := by exact { x := _ } -- error on exact, "tactic failed, there are unsolved goals"
Last updated: Dec 20 2023 at 11:08 UTC