Zulip Chat Archive

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?

Chris Hughes (Apr 05 2018 at 17:35):

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