unfolding do notation

Stream: lean4

[Bolton Bailey]

From #fpil

do let x ← E1
   Stmt
   ...
   En

translates to

E1 >>= fun x =>
do Stmt
   ...
   En

Is there a way to unfold this in the infoview so that I can see what I'm proving?

[Mario Carneiro]

The pretty printer doesn't do that much in terms of re-folding do notation, it is just a sequence of bind applications

[Mario Carneiro]

if you set pp.notation false it will disable this but it will also disable a lot of other things so maybe it won't improve the situation

[Bolton Bailey]

Ok, thanks for the suggestion