Ascii name of the rightward triangle operator (▸)

Stream: new members

[Spearman]

What is the Ascii representation of this operator? It's used in Theorem Proving in Lean 4 where it says its a macro but does it have an ascii name?

[Mario Carneiro]

many operators in lean do not have an ascii equivalent, but you can type the triangle operator in a lean-enabled editor using \t

[Mario Carneiro]

in general, you can find out how to type a unicode symbol by hovering over it in vscode