show_term and sorryAx

Stream: general

[Damiano Testa]

I imagine that this is probably not especially problematic, but I found this suggestion amusing:

import Std.Tactic.ShowTerm

example : False := by
  show_term{dsimp only}  -- Try this: exact sorryAx False true

[Kyle Miller]

Just to be clear, this is because the { ... } tactic does sorry for you (and gives the "unsolved goals" message) if there are still goals remaining.

[Damiano Testa]

Ah, I did not realize that in Lean 4 I should use show_term (...) with round brackets! Thanks!

[Kyle Miller]

You don't need brackets at all actually: show_term dsimp only

This works too

  show_term
    rw []
    dsimp only

[Kyle Miller]

There's also the show_term term, so you can do show_term by dsimp only