max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: fix highlighting of #eval etc.

Browse source
This commit is contained in:
Sebastian Ullrich 2020-11-20 16:58:48 +01:00
parent 1e2c0d1d41
commit f6943d9c13
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
doc/highlight.js
View file

@ -1104,6 +1104,7 @@ contains:b}}}());
// original from https://github.com/leanprover-community/highlightjs-lean/blob/master/src/lean.js, BSD 3, (c) 2020 Patrick Massot
hljs.registerLanguage("lean", function(hljs) {
var LEAN_KEYWORDS = {
$pattern: /#?\w+/,
keyword:
'theorem|10 lemma|10 definition def class structure instance ' +
'example inductive coinductive ' +