theorem_proving_in_lean4 icon indicating copy to clipboard operation
theorem_proving_in_lean4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover

`mutual` is not highlighted

Open seanmcl opened this issue 4 months ago • 0 comments

I looked into this a bit and filed an issue here https://github.com/leanprover-community/highlightjs-lean/issues/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.

image

seanmcl avatar Oct 22 '24 20:10 seanmcl