From a44e51ce2ec32610d72c841ee7281c06cd87e6d7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 23 Nov 2020 18:32:39 -0800
Subject: [PATCH] fix: identifiers highlighting and literals

---
 doc/highlight.js | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/highlight.js b/doc/highlight.js
index d8ff0da192..faf8e2748f 100644
--- a/doc/highlight.js
+++ b/doc/highlight.js
@@ -1136,14 +1136,14 @@ hljs.registerLanguage("lean", function(hljs) {
       'have replace at suffices show from ' +
       'congr congr_n congr_arg norm_num ring ',
     literal:
-      'tt ff',
+      'true false',
     meta:
       'noncomputable|10 private protected mutual',
     strong:
       'sorry admit',
   };
 
-  var LEAN_IDENT_RE = /[A-Za-z_][\\w\u207F-\u209C\u1D62-\u1D6A\u2079\']*/;
+  var LEAN_IDENT_RE = /[A-Za-z_][\\w\u207F-\u209C\u1D62-\u1D6A\u2079\'0-9]*/;
 
   var DASH_COMMENT = hljs.COMMENT('--', '$');
   var MULTI_LINE_COMMENT = hljs.COMMENT('/-[^-]', '-/');