#see コマンド実装例

暗黙インスタンスを見つけているだけ？

see: https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Need.20help.20understanding.20ring_nf/near/497758440

import Lean

open Lean Elab Command Meta

syntax (name := see) "#see" term : command

@[command_elab see]
def elabShow : CommandElab
  | `(#see%$tk $term) => withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_show do
    -- -- show signature for `#check id`/`#check @id`
    -- if let `($id:ident) := term then
    --   try
    --     for c in (← realizeGlobalConstWithInfos term) do
    --       addCompletionInfo <| .id term id.getId (danglingDot := false) {} none
    --       logInfoAt tk <| .signature c
    --       return
    --   catch _ => pure ()  -- identifier might not be a constant but constant + projection
    let e ← Term.elabTerm term none
    Term.synthesizeSyntheticMVarsNoPostponing (ignoreStuckTC := true)
    -- Users might be testing out buggy elaborators. Let's typecheck before proceeding:
    withRef tk <| Meta.check e
    let e ← Term.levelMVarToParam (← instantiateMVars e)
    if e.isSyntheticSorry then
      return
    let type ← inferType e
    let str : MessageData ← e.withApp fun f xs ↦
      return xs.foldl (fun m n ↦ m ++ m!" {n}") m!"{f}"
    logInfoAt tk <| str ++ m!" : {type}"
  | _ => throwUnsupportedSyntax

/--
info: @OfScientific.ofScientific Float instOfScientificFloat 27 true 2 : Float
-/
#guard_msgs in
#see 0.27

Start with the #see syntax and the elabShow command elaborator in the issue, then trace its uses of Term.elabTerm, Meta.check, and inferType. Compare the implementation with the linked Zulip discussion and confirm what the #see 0.27 output represents. Done means the example clearly documents whether implicit instances are being found.