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