syntax highlighter

Stream: Codewars

[Kenny Lau]

What's the syntax highlighter used? It doesn't highlight theorem or lemma or by and it doesn't comment out comments /- I am a comment -/

[Shing Tak Lam]

I did some digging into their JS, and I found this line in the file which I think is responsible for syntax highlighting/entry mode

                        case "lean":
                            return "agda";

So I think Lean's using the Agda highlighter right now...

[Shing Tak Lam]

Yeah it does seem to be the case. It highlights constructor and quote which aren't Lean keywords.

[Bryan Gin-ge Chen]

I happen to have a Lean mode for CodeMirror in this Observable notebook. I'll try to split it out into its own repo by the weekend.