pretty printing that preserves types

Stream: mathlib4

[Frederick Pu]

Is there an option so that pretty printing preserves all coercion information?

[Frederick Pu]

ie if you elaborate the pretty printed string you get the original type

[Yury G. Kudryashov]

There is docs#Lean.pp.coercions.types

[Yury G. Kudryashov]

See also other pp options there.

[Aaron Liu]

Having 100% fidelity is pretty hard though

[Frederick Pu]

thx! Are there any other corner cases that could cause the pretty printed string to elaborate to a different type.

[Yury G. Kudryashov]

The round-trip with pretty printing is not 100% accurate, but there are some pp options that improve it.

[Aaron Liu]

For example, if a non-canonical instance was used

[Aaron Liu]

Or some universe metavariables are not solved for

[Yury G. Kudryashov]

(or other implicit argument was supplied via @mythm or mythm (n := _))

[Frederick Pu]

maybe there's a way that everytime you a apply a macro rule for pretty printing you could check if it preserves teh type and if not you don't apply that particular rule or smth. But that would involve changing how the pretty printer works

[Yury G. Kudryashov]

Also, if your expression is complicated enough, Lean may fail to elaborate it using the default elaboration order.

[Frederick Pu]

The broader motivation is that I think being able to extract tactic states as synthetic lemmas is useful for both model parrallelism and the ability to be able to use whole proof models as exact? style tactics

[Yury G. Kudryashov]

E.g., I wouldn't try to round-trip a term you get from a simp call.

[Frederick Pu]

my point is that if you can't pretty print it you just print the raw expr

[Frederick Pu]

so you start printing the raw expr at the first level where the pretty print breaks the type correctness

[Frederick Pu]

i think for tactic states this should be fine

[Frederick Pu]

except for when you use simp or smth to make a member of Fin n or some other subtype. But we can probably make an exception for propositions because of prop extensionality anyways