How to add implication as a theorem to grind?

Stream: new members

[Jakub Nowak]

If the theorem is a field projection, then one can use @[grind cases] on the structure definition. Is it possible to add arbitrary implication as a theorem to grind? This questions stems from that one: #general > grind no error, but not using lemma

opaque foo : Type
opaque bar : Prop

/-- error: invalid `grind` theorem, failed to find an usable pattern using different modifiers -/
#guard_msgs in
@[grind]
axiom bar_of_foo (h : foo) : bar

example (h : foo) : bar := by
  grind -- fails

[Jakub Nowak]

I.e. I would want grind to add bar and bar ↔ True to e-tree after discovering some foo instance. I think that would mean such a pattern? But it doesn't work.

grind_pattern bar_of_foo => h

[Jakub Nowak]

To clarify what I mean by it working with field projection. In the following case foo.bar_of_foo is a field projection and I can make grind use it by tagging foo with @[grind cases].

opaque bar : Prop

@[grind cases]
structure foo : Type where
  bar_of_foo : bar

/-- info: foo.bar_of_foo (self : foo) : bar -/
#guard_msgs in
#check foo.bar_of_foo

example (h : foo) : bar := by grind