Single `.` in place of proof

Stream: new members

[Eric Wieser]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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]

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]

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

[Utensil Song]

@Eric Wieser Check out https://leanprover.zulipchat.com/#narrow/stream/240192-Berkeley-Lean.20Seminar/topic/Periods.20at.20the.20end.20of.20statements