set complement in browser version of Lean

Stream: general

[Jeremy Avigad]

My students have pointed out to me that the set complement notation sᶜ doesn't work in the browser version of Lean. At least, \compl, \^c, and \complement don't work. As a workaround, I am telling them to write s.compl.

• Can this be fixed?
• Is there a better workaround?

[Johan Commelin]

@Bryan Gin-ge Chen :up:

[Bryan Gin-ge Chen]

@Jeremy Avigad Sorry about that, the unicode translation file being used was out of date. The shortcuts should hopefully work in the web editor in 3 hours or so.

[Jeremy Avigad]

Thanks! No problem.

[Eric Wieser]

While we're on the browser version - I find that if I have 12345|67890ABC where | is the cursor, and type \forall , then the result is 12345∀ 67890A|BC- the cursor jumps very annoyingly

[Bryan Gin-ge Chen]

Thanks for the report! The part of the code that handles cursor positioning after unicode translation is definitely a bit hacky. Do you mind making an issue at https://github.com/leanprover-community/lean-web-editor ?

[Eric Wieser]

Done. Github blew up on me so there is a duplicate issue