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

chore: missing keywords

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-09 11:38:12 -08:00
parent 4390de88b8
commit 095ee9f8d2
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/highlight.js
View file

@ -1118,7 +1118,7 @@ hljs.registerLanguage("lean", function(hljs) {
'syntax macro_rules macro ' +
'fun ' +
'#check #check_failure #eval #reduce #print ' +
'section namespace end infix prefix ',
'section namespace end infix infixl infixr postfix prefix ',
built_in:
'Type Prop|10 Sort rw|10 rewrite rwa erw subst substs ' +
'simp dsimp simpa simp_intros finish using generalizing ' +