the empty function

Stream: general

[Bernd Losert]

Does mathlib have an empty function, i.e. something of type empty -> X? Also, how would you define this as a lambda?

[Eric Wieser]

It's docs#empty.elim

[Bernd Losert]

Ah. Makes sense.

[Pedro Minicz]

empty.rec also does the trick. You can usually find such functions using library_search or suggest.

import tactic

variables (α : Type) (e : empty)

#check (empty.rec _ e : α)

example : empty → α := by library_search
example : empty → α := by suggest
example : empty → α := empty.rec (λ (n : empty), α)

[Yakov Pechersky]

import logic.unique

example (X : Type*) : empty → X .

[Eric Wieser]

If you have x : X to hand, you can just use λ _ : empty, x. If X is also empty, then you can't write it as a lambda and you have to use empty.rec

[Yakov Pechersky]

Again, equation compiler trickery. Since empty has no constructors, . means "discharge all cases... oh wait, there are no cases".

[Yakov Pechersky]

In tactic mode (don't use tactic mode for most data definitions):

example (X : Type*) : empty → X := λ x, by cases x

[Yakov Pechersky]

(Also, X : Sort* works here of course)

[Eric Wieser]

Ah, you can write it as a lambda after all:

variables {X : Sort*}
#check (λ e : empty, (match e with end : X))

Where match e with end is just a really verbose version of the . Yakov used.

[Bernd Losert]

Nice. Thanks folks.

[Adam Topaz]

@Bernd Losert you should also know about the difference between docs#empty and docs#pempty

[Adam Topaz]

I don't know what you're using this for, but if you want universe polymorphic constructions, then pempty is the way to go.

[Mario Carneiro]

By the way, mathlib4 introduces the syntax fun. (or λ.) as a term level equivalent for the example (X : Type*) : empty → X . trick (which doesn't work in lean 4), so you can write example (X : Type*) : Empty → X := λ. in lean 4 (which macro expands to fun x => match x with. like Eric's version).