withImportModules + `#check`/`#print`

Stream: metaprogramming / tactics

[Yury G. Kudryashov]

How do I (a) #check; (b) #print (to a string or to stdout) a declaration from withImportModules? #xy: I have something like

unsafe def main (_ : List String) : IO Unit := do
  initSearchPath (← findSysroot)
  withImportModules #[{module := `Mathlib}] {} (trustLevel := 1024) fun env => do
    let names : Array String := (env.constants.fold · #[]) fun ar c _ ↦
      if isAutoDecl env c then ar else ar.push c.toString -- here `isAutoDecl` is a pure version of Batteries' function
    for name in names.qsortOrd do
      IO.println name

but I want to pretty print the type of the theorem named name instead.

[Damiano Testa]

You could try using docs#Lean.MessageData.signature, maybe?