Print all instances on a type

Stream: general

[Nir Paz]

When learning about a new type I like to see what instances are defined on it (until now by grepping mathlib), is there a way to show all of them? It looks like lean3 had #print instances, but it doesn't work anymore.

[Alex J. Best]

There isn't a command for that (yet) as far as I know. But you can visit the docs which does have a list for each type in mathlib eg docs#Nat, under the heading " Instances for "

[Nir Paz]

Thanks, this is great!

[Adam Topaz]

We also have the #synth command if you want to check whether a type has a particular instance

[Riccardo Brasca]

Alex J. Best said:

There isn't a command for that (yet) as far as I know. But you can visit the docs which does have a list for each type in mathlib eg docs#Nat, under the heading " Instances for "

Something must be a little wrong, since I see instances like this one

[Riccardo Brasca]

Maybe because there is "nat" in the name?

[Adam Topaz]

yeah that looks like a bug in doc-gen4

[Eric Wieser]

I would be very sad to find out that the instance list is using name matching...

[Eric Wieser]

In Lean3 it genuinely checked the types

[Adam Topaz]

ping @Henrik Böving

[Henrik Böving]

Quack

[Riccardo Brasca]

It also lists docs#IccManifold

[Alex J. Best]

EuclideanHalfSpace at least has a nat in the type, maye the DoldKan instance does too?

[Henrik Böving]

doc-gen4 does check if "Nat occurs anywhere within the type of the instance":

def getInstanceTypes (typ : Expr) : MetaM (Array Name) := do
  let (_, _, tail) ← forallMetaTelescopeReducing typ
  let args := tail.getAppArgs
  let (_, names) ← args.mapM (Expr.forEach · findName) |>.run .empty
  return names
where
  findName : Expr → StateRefT (Array Name) MetaM Unit
    | .const name _ => modify (·.push name)
    | .sort .zero => modify (·.push "_builtin_prop")
    | .sort (.succ _) => modify (·.push "_builtin_typeu")
    | .sort _ => modify (·.push "_builtin_sortu")
    | _ => return ()

def InstanceInfo.ofDefinitionVal (v : DefinitionVal) : MetaM InstanceInfo := do
  let mut info ← DefinitionInfo.ofDefinitionVal v
  let some className ← isClass? v.type | panic! s!"isClass? on {v.name} returned none"
  if let some instAttr ← getDefaultInstance v.name className then
    info := { info with attrs := info.attrs.push instAttr }
  let typeNames ← getInstanceTypes v.type
  return {
    toDefinitionInfo := info,
    className,
    typeNames
  }

[Henrik Böving]

I can turn this down and e.g. use a telescope and only look at the type at the end of an arrow if you want? Or something else entirely?

[Eric Wieser]

Maybe we want two headings, "instances for this type" and "instances involving this type, where the former is only things with an explicit argument equal to (an application of) the type?

[Kyle Miller]

Maybe this is a possibility?

import Lean

open Lean Meta

def getInstanceTypes (typ : Expr) : MetaM (Array Name) := do
  let (_, _, tail) ← forallMetaTelescopeReducing typ
  let args := tail.getAppArgs
  let (_, bis, _) ← forallMetaTelescopeReducing (← inferType tail.getAppFn)
  let (_, names) ← (bis.zip args).mapM findName |>.run .empty
  return names
where
  findName : BinderInfo × Expr → StateRefT (Array Name) MetaM Unit
    | (.default, .sort .zero) => modify (·.push "_builtin_prop")
    | (.default, .sort (.succ _)) => modify (·.push "_builtin_typeu")
    | (.default, .sort _) => modify (·.push "_builtin_sortu")
    | (.default, e) =>
      match e.getAppFn with
      | .const name .. => modify (·.push name)
      | _ => return ()
    | _ => return ()

set_option autoImplicit true

def foo (t1 t2 : Type) : Prop := True
theorem baz : foo Nat (Fin n) := trivial

#eval do getInstanceTypes (← inferType (.const ``baz []))
-- #[`Nat, `Fin]

[Kyle Miller]

It takes each explicit argument and returns its head constant

[Henrik Böving]

I added this algorithm to doc-gen, it'll be up on mathlib4_docs in a bit (when this ends: https://github.com/leanprover-community/mathlib4_docs/actions/runs/6760311745/job/18373945758) so you can see if its more to your liking