ある項がインスタンスになるような型クラスをすべて列挙するコマンド

Zulip: > All instances satisfied by a type

elab "#list_instances" var:term : command => runTermElabM fun xs => do
  let vvar ← elabTerm var none
  let ce := classExtension.getState (← getEnv)
  let mut insts := #[]
  for (a, _) in ce.outParamMap do
    let const ← getConstInfo a
    match const.type with
    | .forallE _ (.sort _) (.sort _) _ =>
      let mut exp : Expr := default
      try
        exp ← mkAppM a #[vvar]
      catch _ => continue
      let some synthed ← synthInstance? exp | continue
      insts := insts.push (synthed, exp)
    | _ => pure ()
  let (_, sorted) := ((← insts.mapM fun e => return (← ppExpr e.2).pretty).zip insts).qsort (·.1 < ·.1) |>.unzip
  logInfo <| MessageData.joinSep (sorted.toList.map fun (synthed, expr) => m!"'{expr}' (via '{synthed}')") "\n"

Start with the Zulip discussion linked in the issue and review the embedded #list_instances prototype. The issue does not identify a target file, tests, or an agreed command interface, so first determine where such commands belong and what behavior is expected. Done should include an implemented command and tests covering its instance enumeration and output.