Commit 2023-05-10 00:18 c93011c6

feat: pp_extended_field_notation command to pretty print with dot notation (#3811) The projection notation delaborator that comes from core Lean has some limitations. We introduce a new projection notation delaborator that is able to collapse parent projection sequences, for example x.toC.toB.toA.val into x.val. The other limitation of the delaborator is that it can only handle true projections that do not have any additional arguments. This commit adds a pp_extended_field_notation command to switch on projection notation for specific functions. This command defines app unexpanders that pretty print that function application using dot notation. The app unexpander it produces has a small hack to completely collapse parent projection sequences. Since it is an app unexpander, we do not have access to the actual types, so we use a heuristic that, for example with A.foo, if we are looking at A.foo x.toA y z ... then we can pretty print this as x.foo y z. The projection delaborator is able to collapse parent projection sequences except for the vary last one, so this finishes it off. Note that this heuristic can lead to output that does not round trip if there is a toA function that is not a parent projection that happens to be pretty printed with dot notation.