I'm using Lean4 in VS Code and it has the essential feature of showing me definition of anything I select. Is there some way to also find instances of type class definitions?
For example if I write
#check IsCommutative.comm Or ∨
and hold Cmd key then click on IsCommutative.comm , VS code will take me to
/--
`IsCommutative op` says that `op` is a commutative operation,
i.e. `a ∘ b = b ∘ a`. It is used by the `ac_rfl` tactic.
-/
class IsCommutative {α : Sort u} (op : α → α → α) where
/-- A commutative operation satisfies `a ∘ b = b ∘ a`. -/
comm : (a b : α) → op a b = op b a
but I'd like to see the instance definition for Or.
One way to do this is to use the #synth command to synthesize an instance and print its name. Let's use the Inhabited typeclass as an example.
#synth Inhabited Nat
successfully synthesizes an instance and prints instInhabitedNat in the infoview, which is the name of this instance. Note that in this case it is an automatically generated identifier, whose use in code is normally discouraged, but it's fine for this purpose. You can now
#check instInhabitedNat
and go to its definition to find
instance : Inhabited Nat where
default := Nat.zero
in Prelude.
Regarding the example you gave, the fact that Or is commutative would rather be written IsCommutative Prop Or using the typeclass you mentioned, and it seems to not be the case that Or is an instance thereof, as #synth IsCommutative Prop Or fails.