## Stream: new members

### Topic: Single . in place of proof

#### Eric Wieser (Jul 27 2020 at 13:21):

I just found this in mathlib (modulo notation which I removed to make a #mwe)

theorem cons_ne_nil (a : ℕ) (l : list ℕ) : list.cons a l ≠ list.nil.


What does . mean?

#### Mario Carneiro (Jul 27 2020 at 13:27):

it means nothing, it just ends the definition. The actual proof is an empty pattern match

#### Eric Wieser (Jul 27 2020 at 13:31):

An empty pattern match in that there are zero instances of false to match against?

#### Eric Wieser (Jul 27 2020 at 13:41):

I'm puzzled because it seems there is something to match against:

example (a : ℕ) (l : list ℕ) : list.cons a l ≠ list.nil
| h := begin
sorry
end


#### Mario Carneiro (Jul 27 2020 at 13:47):

It's matching on the equality, and the only constructor for equality, rfl, is not type correct, so no match arms are needed

#### Mario Carneiro (Jul 27 2020 at 13:47):

example (a : ℕ) (l : list ℕ) : list.cons a l ≠ list.nil
| h := by cases h


#### Utensil Song (Jul 27 2020 at 13:53):

Last updated: May 07 2021 at 00:30 UTC