Documentation

Lean.Widget.Basic

Lean.Widget.Basic

Imports

Init
Lean.Message
Lean.Elab.InfoTree
Lean.Server.InfoUtils
Lean.Server.Rpc.Basic

Imported by

Lean.Widget.instTypeNameInfoWithCtx

Lean.Widget.instTypeNameMessageData

Lean.Widget.instTypeNameLocalContext

Lean.Widget.instTypeNameContextInfo

Lean.Widget.instTypeNameTermInfo

instance Lean.Widget.instTypeNameInfoWithCtx :

TypeName Lean.Elab.InfoWithCtx

instance Lean.Widget.instTypeNameMessageData :

TypeName Lean.MessageData

instance Lean.Widget.instTypeNameLocalContext :

TypeName Lean.LocalContext

instance Lean.Widget.instTypeNameContextInfo :

TypeName Lean.Elab.ContextInfo

instance Lean.Widget.instTypeNameTermInfo :

TypeName Lean.Elab.TermInfo