The docs made it seem that a double-backslash was not user definable. It turns out that it's a single backslash that's not user definable; the docs preserved escaping from the Haskell implementation (cf. src/Idris/ParseHelpers.hs:/invalidOperators/). Thanks to @mietek, niklasl2, and @Melvar for pointing this out in #idris.