Inaccessible terms and non-working TPIL example

Stream: new members

[Yakov Pechersky]

I'm continuing to read TPIL, now on Inaccessible terms. The first motivating example in the document throws errors for me. MWE:

variables {α β : Type}
inductive image_of (f : α → β) : β → Type
| imf : Π a, image_of (f a)

open image_of

def inverse {f : α → β} : Π b, image_of f b → α
| .(f a) (imf .(f) a) := a

If I understand correctly, the compiler doesn't know where the a comes from.

[Reid Barton]

Check whether imf actually takes two explicit arguments f and a. The default rules for implicit-ness of constructors changed recently.

[Bryan Gin-ge Chen]

Yeah, looks like one of the recent community versions broke this example, since it works in the old web editor and in a local Lean 3.4.2 project.

[Bryan Gin-ge Chen]

This works (in Lean 3.15.0c):

variables {α β : Type}
inductive image_of (f : α → β) : β → Type
| imf : Π a, image_of (f a)

open image_of

def inverse {f : α → β} : Π b, image_of f b → α
| .(f a) (imf a) := a

[Yakov Pechersky]

I played around with it and got this working:

def inverse {f : α → β} : Π b, image_of f b → α
| b := begin
intros inf,
cases inf with a,
exact a
end

Should the TPIL document be edited?

[Yakov Pechersky]

I guess that's equivalent to Bryan's code.

[Bryan Gin-ge Chen]

Sure, I think @Jeremy Avigad is pretty receptive to PRs here.

[Jeremy Avigad]

Yeah, the problem is that TPIL is still running with Lean 3.4.2. @Bryan Gin-ge Chen I suppose I should update it to use the online community web editor? It shouldn't be too hard, but it will take me a few days to get to it.