go to typeclass instance, not notation definition

Stream: new members

[Moritz R]

Is there a way to quickly go from e.g.

def evenNonrec (k : Nat) : Prop :=
  k % 2 = 0

to the definition of % that applies in my current context?
In 90% of the cases i do not want go to definition to show me
macro_rules | `($x % $y) => `(binop% HMod.hMod $x $y).
Rather i want to see

instance instMod : Mod Nat := ⟨Nat.mod⟩

or even

@[extern "lean_nat_mod"]
protected def mod : @& Nat → @& Nat → Nat
  /-
  Nat.modCore is defined by well-founded recursion and thus irreducible. Nevertheless it is
  desirable if trivial `Nat.mod` calculations, namely
  * `Nat.mod 0 m` for all `m`
  * `Nat.mod n (m+n)` for concrete literals `n`
  reduce definitionally.
  This property is desirable for `Fin n` literals, as it means `(ofNat 0 : Fin n).val = 0` by
  definition.
   -/
  | 0, _ => 0
  | n@(_ + 1), m =>
    if m ≤ n -- NB: if n < m does not reduce as well as `m ≤ n`!
    then Nat.modCore n m
    else n

[Kyle Miller]

I think you might just have to wait for the next release in a couple weeks: #rss > Recent Commits to lean4:master @ 💬

[Moritz R]

perfect!