@leanprover/infoview
    Preparing search index...

    Type Alias InteractiveDiagnostic

    InteractiveDiagnostic: Omit<LeanDiagnostic, "message"> & {
        message: TaggedText<MsgEmbed>;
    }

    Settings
    Member Visibility