TorchLean API

Docs HomeGuideExamplesGraphs

ProofWidgets.Demos.Macro

Widgets in macros #

Macros may expand to commands or terms that end up saving widget info, but the syntax to which the widget info is associated must be marked as canonical for the widget to be displayed.

source
def Lean.SourceInfo.mkCanonical :
SourceInfo → SourceInfo
Instances For
    source
    def Lean.Syntax.mkInfoCanonical :
    Syntax → Syntax
    Instances For
      source
      def Lean.TSyntax.mkInfoCanonical {k : SyntaxNodeKinds} :
      TSyntax k → TSyntax k
      Instances For
        source
        def «command#browse_» :
        Lean.ParserDescr
        Instances For