copying pp output leads to error

Stream: general

[Kenny Lau]

instance : has_coe_to_fun bool :=
⟨λ _, ℕ → ℕ, λ _, id⟩

example : ff 0 = tt 0 := _ -- ⇑ff 0 = ⇑tt 0

example : ⇑ff 0 = ⇑tt 0 := _
/-
function expected at
  ⇑tt
term has type
  has_coe_to_fun.F tt
-/

[Kenny Lau]

if the pretty printer gives ⇑ff 0 = ⇑tt 0, why can't I use it?

[Kevin Buzzard]

because nobody formalised the proof that the prettyprinter is equal to the inverse of the elaborator, and indeed it's not true.

[Kenny Lau]

I imagine this might cause some confusion to newcomers (but again what doesn't)

[Kevin Buzzard]

You can fix it by setting some pp options, e.g. pp.all true or pp.coercions false