## Stream: general

### Topic: def using dot

#### Chris Hughes (Apr 05 2018 at 16:31):

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 (Apr 05 2018 at 16:31):

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

#### Simon Hudon (Apr 05 2018 at 17:27):

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 (Apr 05 2018 at 17:32):

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

#### Simon Hudon (Apr 05 2018 at 17:34):

You mean with the dot or just pattern matching definitions?

With the dot

#### Simon Hudon (Apr 05 2018 at 17:43):

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 (Apr 05 2018 at 17:48):

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

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


#### Gabriel Ebner (Apr 05 2018 at 17:49):

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 (Apr 05 2018 at 17:51):

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 (Apr 05 2018 at 17:55):

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).


Last updated: Aug 03 2023 at 10:10 UTC