Zulip Chat Archive

Stream: general

Topic: Bug in library_search?


view this post on Zulip Yevhenii Diomidov (Feb 07 2021 at 00:13):

example {α : Type} (a : α) : punit  α := by library_search -- Try this: refine punit.rec a
example {α : Type} (a : α) : punit  α := by refine punit.rec a
  -- type mismatch at application `punit.rec a` term `a` has type `α : Type` but is expected to have type `?m_1 punit.star : Sort ?`

view this post on Zulip Mario Carneiro (Feb 07 2021 at 00:22):

more like a bug in pretty printing; lean has an issue with printing terms that don't re-parse at the same level of explicitness

view this post on Zulip Bryan Gin-ge Chen (Feb 07 2021 at 00:24):

Some more examples:

example {α : Type} (a : α) : punit  α := punit.rec a -- same error as above
example {α : Type} (a : α) : punit  α := by refine punit.rec (by exact a) -- works
example {α : Type} (a : α) : punit  α := punit.rec (by exact a) -- also works

view this post on Zulip Mario Carneiro (Feb 07 2021 at 00:24):

this isn't likely to be fixed in lean 3; lean 4 has a proper support for this through a "delaborator" that can add only just enough implicit information to parse correctly

view this post on Zulip Mario Carneiro (Feb 07 2021 at 00:26):

when writing terms manually, the suggested fix is \lam x, punit.rec a x


Last updated: May 11 2021 at 23:11 UTC