Zulip Chat Archive

Stream: general

Topic: Stray `.` in goal view


view this post on Zulip Eric Wieser (Mar 25 2021 at 17:28):

What's going on here?

import data.finset.basic

theorem foo (m: ) :  {X Y : finset (fin m  )},
  X  ({} : set (finset (fin m  )))  Y  X  Y  ({} : set (finset (fin m  )))
| X Y rfl := sorry -- Y ⊆ .∅ → Y ∈ {∅}

What's the .∅ coming from?

view this post on Zulip Mario Carneiro (Mar 25 2021 at 17:29):

That's most likely a remnant of the inaccessible pattern in place of X

view this post on Zulip Eric Wieser (Mar 25 2021 at 17:29):

It goes away if I put by before sorry

view this post on Zulip Eric Wieser (Mar 25 2021 at 17:30):

But not if I use id sorry

view this post on Zulip Mario Carneiro (Mar 25 2021 at 17:30):

Here's an example of using an inaccessible pattern:

theorem foo (m: ) :  {X Y : finset (fin m  )},
  X  ({} : set (finset (fin m  )))  Y  X  Y  ({} : set (finset (fin m  )))
| .() Y rfl := sorry -- Y ⊆ .∅ → Y ∈ {∅}

view this post on Zulip Mario Carneiro (Mar 25 2021 at 17:31):

this looks like a side effect of the way the printing of the expected type works


Last updated: May 12 2021 at 05:19 UTC