Zulip Chat Archive

Stream: general

Topic: exact and new goals


view this post on Zulip 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: May 14 2021 at 03:27 UTC