## Stream: general

### Topic: pp.unambiguous

#### Johan Commelin (May 30 2020 at 14:23):

How hard would it be to write a tactic that takes an expr and prints a string that is close to the standard pretty printed version, but ready for copy-pasting into the current editor window?

#### Johan Commelin (May 30 2020 at 14:29):

Typical examples are ambiguous 0 that need a type ascription

#### Mario Carneiro (May 30 2020 at 14:29):

it needs more than a type ascription in general

why?

#### Mario Carneiro (May 30 2020 at 14:30):

I would start from pp.all as a baseline

#### Mario Carneiro (May 30 2020 at 14:31):

You can try to take pp.all output and progressively try to remove @ signs while ensuring that the elaborator still produces the right term, but this is pretty expensive since you have to typecheck hundreds of variations of the term

#### Mario Carneiro (May 30 2020 at 14:32):

Johan Commelin said:

why?

You could have a zero with a non-canonical instance, or one that was provided manually and can't be found by instance search

#### Johan Commelin (May 30 2020 at 14:39):

Mario Carneiro said:

You can try to take pp.all output and progressively try to remove @ signs while ensuring that the elaborator still produces the right term, but this is pretty expensive since you have to typecheck hundreds of variations of the term

Expensive is fine if it's only used occasionally, say in extract_goal.

#### Jason Rute (May 30 2020 at 14:39):

I believe Lean 4 is making sure the pp.all round trip succeeds. See https://github.com/leanprover/lean4/blob/50fc9610379243e419f75de7e281cbeb61287324/src/Lean/Delaborator.lean

#### Jason Rute (May 30 2020 at 14:41):

Sorry, I misunderstood. You want something closer to standard pp.

#### Mario Carneiro (May 30 2020 at 14:42):

It's not hard to make something like pp.all that round-trips. I am pretty sure the "delaborator" is doing what I outlined above, trying to get closer to an unmarked term

#### Mario Carneiro (May 30 2020 at 14:47):

I think if you design it well you can get delaboration to be "only" as expensive as elaboration. (Still pretty expensive for something that is doing printing...)

Last updated: May 17 2021 at 22:15 UTC