grind with hashes

Stream: lean4

[Damiano Testa]

Following the PRs on grind (e.g. lean4#10709), I noticed that try? can now produce grind-scripts involving hashes.

/--
info: Try these:
  [apply] grind
  [apply] grind only [#b0f4, #50fc]
  [apply] grind only
  [apply] grind =>
    cases #b0f4
    · cases #50fc
    · cases #50fc <;> lia
-/
#guard_msgs in
example (p : Nat → Prop) (x y z w : Int) :
    (x = 1 ∨ x = 2) →
    (w = 1 ∨ w = 4) →
    (y = 1 ∨ (∃ x : Nat, y = 3 - x ∧ p x)) →
    (z = 1 ∨ z = 0) → x + y ≤ 6 := by
  try?

[Damiano Testa]

Mostly due to this being a very new feature, I wonder if using them is expected/recommended/still to be tested.

[Damiano Testa]

Also, I love the new try?!

[Chris Henson]

In turn, I think this is the case because grind? has had this behavior since the hashes were introduced. I asked a similar question at the time, but I don't believe there was a definitive answer.