## Stream: general

### Topic: Stray . in goal view

#### 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?

#### Mario Carneiro (Mar 25 2021 at 17:29):

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

#### Eric Wieser (Mar 25 2021 at 17:29):

It goes away if I put by before sorry

#### Eric Wieser (Mar 25 2021 at 17:30):

But not if I use id sorry

#### 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 ∈ {∅}


#### 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