{motive : Lean.Lsp.CompletionOptions → Sort u} →
  ((triggerCharacters? allCommitCharacters? : Option (Array String)) →
      (resolveProvider : Bool) →
        motive
          { triggerCharacters? := triggerCharacters?, allCommitCharacters? := allCommitCharacters?,
            resolveProvider := resolveProvider }) →
    (t : Lean.Lsp.CompletionOptions) → motive t