TorchLean API

Docs HomeGuideExamplesGraphs

Lean.Widget.Basic

source
@[implicit_reducible]
instance Lean.Widget.instTypeNameInfoWithCtx :
TypeName Elab.InfoWithCtx
source
@[implicit_reducible]
instance Lean.Widget.instTypeNameLocalContext :
TypeName LocalContext
source
@[implicit_reducible]
instance Lean.Widget.instTypeNameContextInfo :
TypeName Elab.ContextInfo
source
@[implicit_reducible]
instance Lean.Widget.instTypeNameTermInfo :
TypeName Elab.TermInfo