{motive : Lean.Elab.CompletionInfo → Sort u} →
  (t : Lean.Elab.CompletionInfo) →
    ((stx partialId : Lean.Syntax) → motive (Lean.Elab.CompletionInfo.errorName stx partialId)) →
      (Nat.hasNotBit 64 t.ctorIdx → motive t) → motive t