@[implicit_reducible]

instance Lean.Widget.instTypeNameInfoWithCtx : TypeName Elab.InfoWithCtx

Equations

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

@[implicit_reducible]

instance Lean.Widget.instTypeNameLocalContext : TypeName LocalContext

Equations

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

@[implicit_reducible]

instance Lean.Widget.instTypeNameContextInfo : TypeName Elab.ContextInfo

Equations

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

@[implicit_reducible]

instance Lean.Widget.instTypeNameTermInfo : TypeName Elab.TermInfo

Equations

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