"\\\"\$\\\/\b\f\n\r\t \u2200(a : Type) \u2192 a"