rw through abbrev

Stream: new members

[Moritz R]

Does rw not see through abbreviations?
I have this

/-- A term `t` with variables indexed by `α` can be evaluated by giving a value
to each variable using `v`. -/
def eval {I : Interpretation F} (t : Term F α) (w : α → I) : I :=
  match t with
  | .var k => w k
  | .func _ f ts => I.funInter f (fun i ↦ (ts i).eval w)

/-- A version of `Term.eval` that takes the Interpretation to be used
    as an explicit second argument. -/
abbrev evalIn (t : Term F α) (I : Interpretation F) (w : α → I) :
    I :=
  @Term.eval α F I t w

now i am in a situation where i have a t1.eval w that i want to rewrite with an equation
t1.evalIn (hInter I) w = .... I checked that the first term really uses the same Interpretation as the evalIn term.
If i unfold evalIn in my rewriting equation, i can rewrite with it.
If i dont unfold it, rewriting fails

[Aaron Liu]

rw does not see through abbrevs in the same way that simp does

[Moritz R]

ohje

[Moritz R]

Is there a good reason for this?

[Aaron Liu]

from docs#Lean.Meta.kabstract:

We detect subterms equivalent to p using key-matching. That is, only perform isDefEq tests when the head symbol of subterm is equivalent to head symbol of p.

[Aaron Liu]

this is an optimization so we don't have to check every subterm

[Moritz R]

Anything i can do to make my abbrev extra-see-through?

[Moritz R]

unfortunately it is the head symbol here

[Moritz R]

and will always be

[Aaron Liu]

you could do a notation

[Moritz R]

And then a custom delaborator again, so that it doesn't always show up, but only if there is possbile ambiguity in the context? i.e. two elements of type Interpretation _

[Aaron Liu]

see for example the notation for IsOpen that makes the topology explicit, docs#Topology.IsOpen_of

[Moritz R]

I see a pattern in our discussions :D

[Aaron Liu]

Moritz R said:

And then a custom delaborator again, so that it doesn't always show up, but only if there is possbile ambiguity in the context? i.e. two elements of type Interpretation _

this might be more difficult, but should be doable