Documentation

Lean.Widget.Basic

source
instance Lean.Widget.instTypeNameInfoWithCtx :
TypeName Elab.InfoWithCtx
Equations
    source
    instance Lean.Widget.instTypeNameLocalContext :
    TypeName LocalContext
    Equations
      source
      instance Lean.Widget.instTypeNameContextInfo :
      TypeName Elab.ContextInfo
      Equations
        source
        instance Lean.Widget.instTypeNameTermInfo :
        TypeName Elab.TermInfo
        Equations