Zulip Chat Archive
Stream: general
Topic: copying pp output leads to error
Kenny Lau (Jun 18 2020 at 13:35):
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 (Jun 18 2020 at 13:35):
if the pretty printer gives ⇑ff 0 = ⇑tt 0
, why can't I use it?
Kevin Buzzard (Jun 18 2020 at 13:37):
because nobody formalised the proof that the prettyprinter is equal to the inverse of the elaborator, and indeed it's not true.
Kenny Lau (Jun 18 2020 at 13:38):
I imagine this might cause some confusion to newcomers (but again what doesn't)
Kevin Buzzard (Jun 18 2020 at 13:38):
You can fix it by setting some pp options, e.g. pp.all true or pp.coercions false
Last updated: Dec 20 2023 at 11:08 UTC