Stream: Beginner Questions

Topic: Find definition of instance

Patrick Nicodemus (May 07 2023 at 15:30):

How do I use jedit to find the definition of a typeclass instance for a type?

Right now I'm looking at the Category theory for ZFC article in AFP, CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Ordinal.thy
It contains the following definition:

definition ordinal_arrs :: "V ⇒ V"
  where "ordinal_arrs A ≡ set {[a, b]⇩∘ | a b. a ∈⇩∘ A ∧ b ∈⇩∘ A ∧ a ≤ b}"

I see that ≤ is notation for Orderings.ord_class.less_eq. I also see that by using print_classes I can get a list of all typeclass instances and search through this list to find the one that's relevant.

class ord:
  supersort: type
  parameters:
    less_eq :: 'a ⇒ 'a ⇒ bool
    less :: 'a ⇒ 'a ⇒ bool
  instances:
    (...)
    Predicate.pred :: (type) ord
    String.literal :: ord
    V :: ord
    (...)

So I see that V is declared as an instance. However I do not understand how to navigate to the definition of the instance for V from this. I have tried using the Query tool to search for ord_V_def or V_ord_defbut nothing comes up.

Last updated: Apr 28 2024 at 08:19 UTC