"\\\"\$\\\/\b\f\n\r\t\u{1D11E} \u2200(a : Type) \u2192 a"