Eric Wieser

Just to note this now also impacts `eval%` in mathlib: ```lean import Mathlib.Tactic.Eval def foo.{u} (x : PUnit.{u}) : Nat := 37 -- fails without this PR def bar.{u} (x...

This worked fine in my own repository - any idea why it wouldn't be working fine here?

So writing to stdout using a different mechanism to writing to a file handle? Edit: Ah, I get it now.

Would chunking the conversion help here?

I worked around this downstream by just calling `tail -n 1 export.json`, which does the job of separating lean diagnostics from json output. It's ugly, but far easier that digging...

Right - so this is presumably an issue in the pretty-printer and not the docs at all. Should this issue be moved to the lean repo?

Perhaps show implicit arguments if they cannot be inferred unambiguously

Looks pretty damning, thanks for the detailed report. Issues with delta cycles indeed look to be the culprit.

I'd argue that rebasing from a string template is as weird as including one, since a `rebase` gets translated to an `include`: ``` python Foo: {{foo}} % # hypothetical api...

I was getting confused by the lack of syntax highlighting and syntax error by the OP, and assumed I was looking at tpl code not raw python. Oops. I now...