{motive : Lean.Lsp.CompletionItem → Sort u} →
  (t : Lean.Lsp.CompletionItem) →
    ((label : String) →
        (detail? : Option String) →
          (documentation? : Option Lean.Lsp.MarkupContent) →
            (kind? : Option Lean.Lsp.CompletionItemKind) →
              (textEdit? : Option Lean.Lsp.InsertReplaceEdit) →
                (sortText? : Option String) →
                  (data? : Option Lean.Json) →
                    (tags? : Option (Array Lean.Lsp.CompletionItemTag)) →
                      motive
                        { label := label, detail? := detail?, documentation? := documentation?, kind? := kind?,
                          textEdit? := textEdit?, sortText? := sortText?, data? := data?, tags? := tags? }) →
      motive t