Exploding sorry

Stream: general

[Eric Wieser]

This does something pretty surprising:

example : sorry := by
  rw [show 1 = 0 + 1 from rfl]

⊢ sorry
  (((((((((((`«external:file:///project/mathlib-demo.lean».num (0 + 1)).num 10).num (0 + 1)).num 15).num 10).num 15).str
                    "_sorry").str
                "_@").str
            "external:file:///project/mathlib-demo.lean").str
        "_hyg").num
    5)

[Eric Wieser]

@Kyle Miller, should named sorries use raw numerals instead of OfNat?