def using dot

Stream: general

[Chris Hughes]

How does this definition work?

def  empty.elim {C : Sort*} : empty → C.

What does the dot at the end do? I haven't seen that before.

[Kenny Lau]

"it's too obvious I don't even wanna write "rfl""

[Simon Hudon]

I don't think that's it. I think it's a definition by pattern matching and empty has no constructors. I haven't seen . used that way before but it looks to me like it signals that we're done with the pattern matching.

[Chris Hughes]

How does this notation work in general, for things with constructors?

[Simon Hudon]

You mean with the dot or just pattern matching definitions?

[Chris Hughes]

With the dot

[Simon Hudon]

I haven't seen many more examples but I found these:

lemma not_succ_le_zero : ∀ (n : ℕ), succ n ≤ 0 → false
.
lemma bool.ff_ne_tt : ff = tt → false
.

I think you just put it in instead of a pattern matching to signal that there are no constructors.

[Gabriel Ebner]

In general the dot is an optional command delimiter, you can always use it if you want:

def foo : ℕ → ℕ | x := x+1.

[Gabriel Ebner]

If you want to write a definition using pattern matching and you have zero equations, then the dot is mandatory. The examples above have zero equations.

[Gabriel Ebner]

In case you didn't know, this definition syntax is essentially just sugar for a nested match. Here it is maybe clearer that there are zero equations:

example {C : Sort*} (h : ff = tt) : C :=
match h with end

[Gabriel Ebner]

To give you an intuition for when this zero-equation magic works, recall that the equation compiler is (ignoring lots and lots of details) a wrapper around the cases tactic. Whenever iterated cases would yield zero subgoals, then you can use this magic.

example : ¬ (∃ n, n < 0).