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

fix: highlight.js

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-24 12:53:54 -08:00
parent 495b6a92e9
commit cf0bb173ad
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
doc/highlight.js
View file

@ -1115,7 +1115,7 @@ hljs.registerLanguage("lean", function(hljs) {
'import open theory prelude renaming hiding exposing ' +
'calc match with do by let extends ' +
'for in unless try catch finally mutual mut return continue break where rec ' +
'syntax macro_rules ' +
'syntax macro_rules macro ' +
'fun ' +
'#check #eval #reduce #print ' +
'section namespace end',
@ -1168,7 +1168,7 @@ hljs.registerLanguage("lean", function(hljs) {
var LEAN_DEFINITION = {
className: 'theorem',
beginKeywords: 'def theorem lemma class instance structure',
end: ':=',
end: ':= | where',
excludeEnd: true,
contains: [
{