Documentation

Lean.Widget.Basic

Imports

Lean.Message
Lean.Elab.InfoTree
Lean.Server.InfoUtils
Lean.Widget.Types
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

Equations

Lean.Widget.instTypeNameContextInfo = Lean.Widget.inst✝

instance Lean.Widget.instTypeNameTermInfo :

TypeName Lean.Elab.TermInfo