CODEWITHSUNDEEP
lean
alagris
alagris

Reputation: 2206

Go to type class instance definition in Lean 4

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.

Upvotes: 2

Views: 689

Answers (1)

Horatiu Cheval
Horatiu Cheval

Reputation: 56

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.

Upvotes: 4

Related Questions