You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I looked into this a bit and filed an issue here leanprover-community/highlightjs-lean#19. We may need to update our version of highlight-js, as it does seem to mark mutual as a keyword of some kind, though not sure it's the right kind to look like it should.
The text was updated successfully, but these errors were encountered:
I looked into this a bit and filed an issue here leanprover-community/highlightjs-lean#19. We may need to update our version of highlight-js, as it does seem to mark
mutual
as a keyword of some kind, though not sure it's the right kind to look like it should.The text was updated successfully, but these errors were encountered: