instance Lean.Widget.instTypeNameInfoWithCtx : TypeName Lean.Elab.InfoWithCtx

Equations

• Lean.Widget.instTypeNameInfoWithCtx = Lean.Widget.inst✝

instance Lean.Widget.instTypeNameMessageData : TypeName Lean.MessageData

Equations

• Lean.Widget.instTypeNameMessageData = Lean.Widget.inst✝

instance Lean.Widget.instTypeNameLocalContext : TypeName Lean.LocalContext

Equations

• Lean.Widget.instTypeNameLocalContext = Lean.Widget.inst✝

instance Lean.Widget.instTypeNameContextInfo : TypeName Lean.Elab.ContextInfo

Equations

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

instance Lean.Widget.instTypeNameTermInfo : TypeName Lean.Elab.TermInfo

Equations

• Lean.Widget.instTypeNameTermInfo = Lean.Widget.inst✝