From 2e01ac508a5221c7165b278262e8512b060566e9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 25 Jun 2019 10:38:12 -0700
Subject: [PATCH] feat(library/init/lean/syntax): primitives for creating and
 testing string and nat literals

---
 library/init/lean/compiler/externattr.lean   |   11 +
 library/init/lean/parser/parser.lean         |    9 +-
 library/init/lean/syntax.lean                |  110 +-
 src/frontends/lean/decl_attributes.cpp       |    8 +-
 src/stage0/init/lean/compiler/externattr.cpp |  119 +-
 src/stage0/init/lean/parser/parser.cpp       |   81 +-
 src/stage0/init/lean/syntax.cpp              | 1029 +++++++++++++++++-
 7 files changed, 1279 insertions(+), 88 deletions(-)

diff --git a/library/init/lean/compiler/externattr.lean b/library/init/lean/compiler/externattr.lean
index 48a8604bb7..56d1a5b218 100644
--- a/library/init/lean/compiler/externattr.lean
+++ b/library/init/lean/compiler/externattr.lean
@@ -42,6 +42,17 @@ structure ExternAttrData :=
 
 @[export lean.mk_extern_attr_data_core] def mkExternAttrData := ExternAttrData.mk
 
+private def syntaxToExternAttrData (s : Syntax) : Except String ExternAttrData :=
+match s with
+| Syntax.missing := Except.ok { entries := [ ExternEntry.adhoc `all ] }
+| Syntax.node _ args _ :=
+  if args.size == 0 then Except.error "unexpected kind of argument"
+  else
+    let i := 0 in
+    -- TODO
+    Except.ok { entries := [] }
+| _ := Except.error "unexpected kind of argument"
+
 -- def mkExternAttr : IO (ParametricAttribute ExternAttrData) :=
 -- registerParametricAttribute `extern "builtin and foreign functions" $ λ env declName stx,
 
diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean
index eb74505f6b..b975692d03 100644
--- a/library/init/lean/parser/parser.lean
+++ b/library/init/lean/parser/parser.lean
@@ -464,9 +464,6 @@ def quotedCharFn : BasicParserFn
     else
       s.mkError "invalid escape sequence"
 
-def strLitKind : SyntaxNodeKind := `strLit
-def numLitKind : SyntaxNodeKind := `numLit
-
 /-- Push `(Syntax.node tk <new-atom>)` into syntax stack -/
 def mkNodeToken (n : SyntaxNodeKind) (startPos : Nat) : BasicParserFn :=
 λ c s,
@@ -477,9 +474,8 @@ let val       := input.extract startPos stopPos in
 let s         := whitespace c s in
 let wsStopPos := s.pos in
 let trailing  := { Substring . str := input, startPos := stopPos, stopPos := wsStopPos } in
-let atom      := Syntax.atom (some { leading := leading, pos := startPos, trailing := trailing }) val in
-let tk        := Syntax.node n (Array.singleton atom) [] in
-s.pushSyntax tk
+let info      := { SourceInfo . leading := leading, pos := startPos, trailing := trailing } in
+s.pushSyntax (mkLit n val (some info))
 
 partial def strLitFnAux (startPos : Nat) : BasicParserFn
 | c s :=
@@ -501,6 +497,7 @@ def decimalNumberFn (startPos : Nat) : BasicParserFn :=
   let i     := s.pos in
   let curr  := input.get i in
   let s :=
+    /- TODO(Leo): should we use a different kind for numerals containing decimal points? -/
     if curr == '.' then
       let i    := input.next i in
       let curr := input.get i in
diff --git a/library/init/lean/syntax.lean b/library/init/lean/syntax.lean
index fa18cd6a1c..a41c4669d5 100644
--- a/library/init/lean/syntax.lean
+++ b/library/init/lean/syntax.lean
@@ -33,6 +33,8 @@ abbrev SyntaxNodeKind := Name
 
 @[pattern] def choiceKind : SyntaxNodeKind := `choice
 @[pattern] def nullKind : SyntaxNodeKind := `null
+def strLitKind : SyntaxNodeKind := `strLit
+def numLitKind : SyntaxNodeKind := `numLit
 
 /- Syntax AST -/
 
@@ -207,19 +209,119 @@ protected partial def formatStx : Syntax → Format
 instance : HasFormat Syntax := ⟨Syntax.formatStx⟩
 instance : HasToString Syntax := ⟨toString ∘ format⟩
 
+end Syntax
+
 /- Helper functions for creating Syntax objects using C++ -/
 
 @[export lean.mk_syntax_atom_core]
 def mkSimpleAtom (val : String) : Syntax :=
-atom none val
+Syntax.atom none val
 
 @[export lean.mk_syntax_ident_core]
 def mkSimpleIdent (val : Name) : Syntax :=
-ident none (toString val).toSubstring val [] []
+Syntax.ident none (toString val).toSubstring val [] []
 
 @[export lean.mk_syntax_list_core]
 def mkListNode (args : Array Syntax) : Syntax :=
-node nullKind args []
+Syntax.node nullKind args []
+
+/- Helper functions for creating string and numeric literals -/
+
+def mkLit (kind : SyntaxNodeKind) (val : String) (info : Option SourceInfo := none) : Syntax :=
+let atom := Syntax.atom info val in
+Syntax.node kind (Array.singleton atom) []
+
+def mkStrLit (val : String) (info : Option SourceInfo := none) : Syntax :=
+mkLit strLitKind val info
+
+def mkNumLit (val : String) (info : Option SourceInfo := none) : Syntax :=
+mkLit numLitKind val info
+
+@[export lean.mk_syntax_str_lit_core]
+def mkStrLitAux (val : String) : Syntax :=
+mkStrLit val
+
+@[export lean.mk_syntax_num_lit_core]
+def mkNumLitAux (val : Nat) : Syntax :=
+mkNumLit (toString val)
+
+def Syntax.isStrLit : Syntax → Option String
+| (Syntax.node k args _) :=
+  if k == strLitKind && args.size == 1 then
+    match args.get 0 with
+    | (Syntax.atom _ val) := some val
+    | _ := none
+  else
+    none
+| _ := none
+
+/- Recall that we don't have special Syntax constructors for storing numeric atoms.
+   The idea is to have an extensible approach where embedded DSLs may have new kind of atoms and/or
+   different ways of representing them. So, our atoms contain just the parsed string.
+   The main Lean parser uses the kind `numLitKind` for storing natural numbers that can be encoded
+   in binary, octal, decimal and hexadecimal format. `isNatLit` implements a "decoder"
+   for Syntax objects representing these numerals. -/
+
+private partial def decodeBinLitAux (s : String) : Nat → Nat → Option Nat
+| i val :=
+  if s.atEnd i then some val
+  else
+    let c := s.get i in
+    if c == '0' then decodeBinLitAux (s.next i) (2*val)
+    else if c == '1' then decodeBinLitAux (s.next i) (2*val + 1)
+    else none
+
+private partial def decodeOctalLitAux (s : String) : Nat → Nat → Option Nat
+| i val :=
+  if s.atEnd i then some val
+  else
+    let c := s.get i in
+    if '0' ≤ c && c ≤ '7' then decodeOctalLitAux (s.next i) (8*val + c.toNat - '0'.toNat)
+    else none
+
+private partial def decodeHexLitAux (s : String) : Nat → Nat → Option Nat
+| i val :=
+  if s.atEnd i then some val
+  else
+    let c := s.get i in
+    if '0' ≤ c && c ≤ '9' then decodeHexLitAux (s.next i) (16*val + c.toNat - '0'.toNat)
+    else if 'a' ≤ c && c ≤ 'f' then decodeHexLitAux (s.next i) (16*val + 10 + c.toNat - 'a'.toNat)
+    else if 'A' ≤ c && c ≤ 'F' then decodeHexLitAux (s.next i) (16*val + 10 + c.toNat - 'A'.toNat)
+    else none
+
+private partial def decodeDecimalLitAux (s : String) : Nat → Nat → Option Nat
+| i val :=
+  if s.atEnd i then some val
+  else
+    let c := s.get i in
+    if '0' ≤ c && c ≤ '9' then decodeDecimalLitAux (s.next i) (10*val + c.toNat - '0'.toNat)
+    else none
+
+private def decodeNatLitVal (s : String) : Option Nat :=
+let len := s.length in
+if len == 0 then none
+else
+  let c := s.get 0 in
+  if c == '0' then
+    if len == 1 then some 0
+    else
+     let c := s.get 1 in
+     if c == 'x' || c == 'X' then decodeHexLitAux s 2 0
+     else if c == 'b' || c == 'B' then decodeBinLitAux s 2 0
+     else if c == 'o' || c == 'O' then decodeOctalLitAux s 2 0
+     else if c.isDigit then decodeDecimalLitAux s 0 0
+     else none
+  else if c.isDigit then decodeDecimalLitAux s 0 0
+  else none
+
+def Syntax.isNatLit : Syntax → Option Nat
+| (Syntax.node k args _) :=
+  if k == strLitKind && args.size == 1 then
+    match args.get 0 with
+    | (Syntax.atom _ val) := decodeNatLitVal val
+    | _ := none
+  else
+    none
+| _ := none
 
-end Syntax
 end Lean
diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp
index 8466b58d9a..c35002eb79 100644
--- a/src/frontends/lean/decl_attributes.cpp
+++ b/src/frontends/lean/decl_attributes.cpp
@@ -79,10 +79,14 @@ expr decl_attributes::parse_attr_arg(parser & p, name const & attr_id) {
 object* mk_syntax_atom_core(object*);
 object* mk_syntax_ident_core(object*);
 object* mk_syntax_list_core(object*);
+object* mk_syntax_str_lit_core(object*);
+object* mk_syntax_num_lit_core(object*);
 
 syntax mk_syntax_atom(string_ref const & s) { return syntax(mk_syntax_atom_core(s.to_obj_arg())); }
 syntax mk_syntax_ident(name const & n) { return syntax(mk_syntax_ident_core(n.to_obj_arg())); }
 syntax mk_syntax_list(buffer<syntax> const & args) { return syntax(mk_syntax_list_core(to_array(args))); }
+syntax mk_syntax_str_lit(string_ref const & s) { return syntax(mk_syntax_str_lit_core(s.to_obj_arg())); }
+syntax mk_syntax_num_lit(nat const & n) { return syntax(mk_syntax_num_lit_core(n.to_obj_arg())); }
 
 syntax decl_attributes::expr_to_syntax(expr const & e) {
     buffer<expr> args;
@@ -98,10 +102,10 @@ syntax decl_attributes::expr_to_syntax(expr const & e) {
             literal const & val = lit_value(arg);
             switch (val.kind()) {
             case literal_kind::Nat:
-                new_args.push_back(mk_syntax_atom(string_ref(val.get_nat().to_std_string())));
+                new_args.push_back(mk_syntax_num_lit(val.get_nat()));
                 break;
             case literal_kind::String:
-                new_args.push_back(mk_syntax_atom(val.get_string()));
+                new_args.push_back(mk_syntax_str_lit(val.get_string()));
                 break;
             }
         } else {
diff --git a/src/stage0/init/lean/compiler/externattr.cpp b/src/stage0/init/lean/compiler/externattr.cpp
index bc95c60887..8188797320 100644
--- a/src/stage0/init/lean/compiler/externattr.cpp
+++ b/src/stage0/init/lean/compiler/externattr.cpp
@@ -27,6 +27,7 @@ obj* l_Lean_ExternEntry_backend(obj*);
 namespace lean {
 obj* nat_sub(obj*, obj*);
 }
+obj* l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___boxed(obj*);
 namespace lean {
 obj* mk_adhoc_ext_entry_core(obj*);
 }
@@ -45,13 +46,15 @@ obj* mk_extern_call_core(obj*, obj*, obj*);
 }
 obj* l_String_Iterator_remainingBytes___main(obj*);
 obj* l_Lean_isExtern___boxed(obj*, obj*);
-obj* l___private_init_lean_compiler_externattr_1__parseOptNum(obj*, obj*, obj*);
+obj* l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__1;
 obj* l_List_foldl___main___at_Lean_mkSimpleFnCall___spec__1(obj*, obj*);
+obj* l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__3;
 namespace lean {
 obj* string_push(obj*, uint32);
 }
 obj* l_Lean_ExternEntry_backend___boxed(obj*);
 obj* l_Lean_expandExternPatternAux___boxed(obj*, obj*, obj*, obj*);
+obj* l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__2;
 namespace lean {
 obj* expand_extern_pattern_core(obj*, obj*);
 }
@@ -75,13 +78,16 @@ namespace lean {
 uint8 nat_dec_eq(obj*, obj*);
 }
 extern obj* l_Prod_HasRepr___rarg___closed__1;
+obj* l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData(obj*);
+obj* l___private_init_lean_compiler_externattr_2__parseOptNum(obj*, obj*, obj*);
 uint8 l_UInt32_decEq(uint32, uint32);
 namespace lean {
 obj* mk_inline_ext_entry_core(obj*, obj*);
 }
 obj* l_Lean_getExternAttrData___boxed(obj*, obj*);
+obj* l_Array_size(obj*, obj*);
 obj* l_Lean_getExternEntryForAux(obj*, obj*);
-obj* l___private_init_lean_compiler_externattr_1__parseOptNum___main(obj*, obj*, obj*);
+obj* l___private_init_lean_compiler_externattr_2__parseOptNum___main(obj*, obj*, obj*);
 obj* l_Lean_getExternEntryForAux___main___boxed(obj*, obj*);
 uint8 l_String_Iterator_hasNext___main(obj*);
 obj* l_Lean_getExternEntryForAux___main(obj*, obj*);
@@ -163,7 +169,102 @@ return x_3;
 }
 }
 }
-obj* l___private_init_lean_compiler_externattr_1__parseOptNum___main(obj* x_1, obj* x_2, obj* x_3) {
+obj* _init_l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__1() {
+_start:
+{
+obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; 
+x_1 = lean::box(0);
+x_2 = lean::box(0);
+x_3 = lean::mk_string("all");
+x_4 = lean_name_mk_string(x_2, x_3);
+x_5 = lean::alloc_cnstr(0, 1, 0);
+lean::cnstr_set(x_5, 0, x_4);
+x_6 = lean::box(0);
+x_7 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_7, 0, x_5);
+lean::cnstr_set(x_7, 1, x_6);
+x_8 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_8, 0, x_1);
+lean::cnstr_set(x_8, 1, x_7);
+x_9 = lean::alloc_cnstr(1, 1, 0);
+lean::cnstr_set(x_9, 0, x_8);
+return x_9;
+}
+}
+obj* _init_l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__2() {
+_start:
+{
+obj* x_1; obj* x_2; obj* x_3; obj* x_4; 
+x_1 = lean::box(0);
+x_2 = lean::box(0);
+x_3 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_3, 0, x_1);
+lean::cnstr_set(x_3, 1, x_2);
+x_4 = lean::alloc_cnstr(1, 1, 0);
+lean::cnstr_set(x_4, 0, x_3);
+return x_4;
+}
+}
+obj* _init_l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__3() {
+_start:
+{
+obj* x_1; obj* x_2; 
+x_1 = lean::mk_string("unexpected kind of argument");
+x_2 = lean::alloc_cnstr(0, 1, 0);
+lean::cnstr_set(x_2, 0, x_1);
+return x_2;
+}
+}
+obj* l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData(obj* x_1) {
+_start:
+{
+switch (lean::obj_tag(x_1)) {
+case 0:
+{
+obj* x_2; 
+x_2 = l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__1;
+return x_2;
+}
+case 1:
+{
+obj* x_3; obj* x_4; obj* x_5; uint8 x_6; 
+x_3 = lean::cnstr_get(x_1, 1);
+x_4 = lean::array_get_size(x_3);
+x_5 = lean::mk_nat_obj(0u);
+x_6 = lean::nat_dec_eq(x_4, x_5);
+lean::dec(x_4);
+if (x_6 == 0)
+{
+obj* x_7; 
+x_7 = l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__2;
+return x_7;
+}
+else
+{
+obj* x_8; 
+x_8 = l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__3;
+return x_8;
+}
+}
+default: 
+{
+obj* x_9; 
+x_9 = l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__3;
+return x_9;
+}
+}
+}
+}
+obj* l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___boxed(obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData(x_1);
+lean::dec(x_1);
+return x_2;
+}
+}
+obj* l___private_init_lean_compiler_externattr_2__parseOptNum___main(obj* x_1, obj* x_2, obj* x_3) {
 _start:
 {
 obj* x_4; uint8 x_5; 
@@ -247,11 +348,11 @@ return x_25;
 }
 }
 }
-obj* l___private_init_lean_compiler_externattr_1__parseOptNum(obj* x_1, obj* x_2, obj* x_3) {
+obj* l___private_init_lean_compiler_externattr_2__parseOptNum(obj* x_1, obj* x_2, obj* x_3) {
 _start:
 {
 obj* x_4; 
-x_4 = l___private_init_lean_compiler_externattr_1__parseOptNum___main(x_1, x_2, x_3);
+x_4 = l___private_init_lean_compiler_externattr_2__parseOptNum___main(x_1, x_2, x_3);
 return x_4;
 }
 }
@@ -295,7 +396,7 @@ else
 obj* x_16; obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_21; obj* x_22; 
 x_16 = l_String_Iterator_next___main(x_3);
 x_17 = l_String_Iterator_remainingBytes___main(x_16);
-x_18 = l___private_init_lean_compiler_externattr_1__parseOptNum___main(x_17, x_16, x_5);
+x_18 = l___private_init_lean_compiler_externattr_2__parseOptNum___main(x_17, x_16, x_5);
 x_19 = lean::cnstr_get(x_18, 0);
 lean::inc(x_19);
 x_20 = lean::cnstr_get(x_18, 1);
@@ -892,6 +993,12 @@ REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "mkInlin
 REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "mkStdExtEntry"), 2, lean::mk_std_ext_entry_core);
 REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "mkForeignExtEntry"), 2, lean::mk_foreign_ext_entry_core);
 REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "mkExternAttrData"), 2, lean::mk_extern_attr_data_core);
+l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__1 = _init_l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__1();
+lean::mark_persistent(l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__1);
+l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__2 = _init_l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__2();
+lean::mark_persistent(l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__2);
+l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__3 = _init_l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__3();
+lean::mark_persistent(l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__3);
 REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "expandExternPatternAux"), 4, l_Lean_expandExternPatternAux___boxed);
 REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "expandExternPattern"), 2, lean::expand_extern_pattern_core);
 REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "mkSimpleFnCall"), 2, l_Lean_mkSimpleFnCall);
diff --git a/src/stage0/init/lean/parser/parser.cpp b/src/stage0/init/lean/parser/parser.cpp
index cd0ca90918..9d298fa957 100644
--- a/src/stage0/init/lean/parser/parser.cpp
+++ b/src/stage0/init/lean/parser/parser.cpp
@@ -70,7 +70,6 @@ obj* l_Lean_Parser_commandParser___elambda__1(obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_regBuiltinCommandParserAttr___closed__1;
 obj* l_Lean_Parser_anyOfFn___boxed(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_longestMatchMkResult(obj*, obj*);
-obj* l_Array_mkArray(obj*, obj*, obj*);
 obj* l_Lean_Parser_andthenFn___rarg(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_ParserState_hasError___boxed(obj*);
 obj* l_Lean_Parser_symbolInfo(obj*, obj*);
@@ -121,6 +120,7 @@ obj* l___private_init_lean_parser_parser_4__tokenFnAux___main(obj*, obj*);
 obj* l_Lean_Parser_rawFn___main___rarg(obj*, uint8, obj*, obj*, obj*);
 obj* l_Lean_Parser_regBuiltinTestParserAttr___closed__2;
 obj* l_Lean_Parser_Parser_inhabited(uint8);
+extern obj* l_Lean_numLitKind;
 obj* l_Lean_Parser_unicodeSymbolFn(uint8);
 obj* l_Lean_Parser_registerBuiltinParserAttribute___lambda__1___closed__4;
 uint8 l_Lean_Parser_TokenConfig_beq___main(obj*, obj*);
@@ -206,7 +206,6 @@ obj* l_Lean_Parser_TokenMap_Inhabited(obj*);
 obj* l_Nat_repr(obj*);
 obj* l_Lean_Parser_mkNodeToken(obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_node(uint8, obj*, obj*);
-obj* l_Lean_Parser_numLitKind;
 obj* l_Lean_Parser_rawFn___main(uint8);
 obj* l_Lean_Parser_andthen___boxed(obj*, obj*, obj*);
 obj* l_Lean_Parser_nodeFn___main___boxed(obj*);
@@ -333,6 +332,7 @@ uint8 l_RBNode_isRed___main___rarg(obj*);
 obj* l_Lean_Parser_satisfyFn___main___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_pushLeadingFn(obj*, obj*, obj*);
 obj* l_List_foldl___main___at_Lean_Parser_addBuiltinLeadingParser___spec__1(obj*, obj*, obj*);
+extern obj* l_Lean_strLitKind;
 obj* l_Lean_Parser_ident___closed__1;
 obj* l_Lean_Parser_addBuiltinLeadingParser___closed__2;
 obj* l_Lean_Parser_Parser_inhabited___lambda__1___boxed(obj*, obj*, obj*);
@@ -528,6 +528,7 @@ obj* l_Lean_Parser_registerBuiltinParserAttribute___lambda__1___closed__1;
 obj* l_Lean_Parser_hexDigitFn(obj*, obj*);
 obj* l_Lean_Parser_takeWhileFn___boxed(obj*, obj*, obj*);
 obj* l_Lean_Parser_insertToken(obj*, obj*, obj*);
+obj* l_Lean_mkLit(obj*, obj*, obj*);
 obj* l_Lean_Parser_trailingParser___boxed(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Name_append___main(obj*, obj*);
 uint8 l_Lean_isIdFirst(uint32);
@@ -544,7 +545,6 @@ obj* l_Lean_Parser_numLitFn(uint8, obj*);
 obj* l_Lean_FileMap_ofString(obj*);
 obj* l_Lean_Parser_isIdCont___main___boxed(obj*, obj*);
 obj* l_Lean_Parser_regBuiltinTestParserAttr___closed__1;
-obj* l_Lean_Parser_strLitKind;
 obj* l_Lean_Parser_sepByFn___main___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_IO_Prim_Ref_reset(obj*, obj*, obj*);
 obj* l___private_init_lean_parser_parser_2__rawAux___main___boxed(obj*);
@@ -4419,30 +4419,10 @@ lean::dec(x_1);
 return x_3;
 }
 }
-obj* _init_l_Lean_Parser_strLitKind() {
-_start:
-{
-obj* x_1; obj* x_2; obj* x_3; 
-x_1 = lean::box(0);
-x_2 = lean::mk_string("strLit");
-x_3 = lean_name_mk_string(x_1, x_2);
-return x_3;
-}
-}
-obj* _init_l_Lean_Parser_numLitKind() {
-_start:
-{
-obj* x_1; obj* x_2; obj* x_3; 
-x_1 = lean::box(0);
-x_2 = lean::mk_string("numLit");
-x_3 = lean_name_mk_string(x_1, x_2);
-return x_3;
-}
-}
 obj* l_Lean_Parser_mkNodeToken(obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
 _start:
 {
-obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_19; 
+obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_15; 
 x_5 = lean::cnstr_get(x_3, 1);
 x_6 = lean::cnstr_get(x_4, 1);
 lean::inc(x_6);
@@ -4467,18 +4447,9 @@ lean::cnstr_set(x_12, 1, x_2);
 lean::cnstr_set(x_12, 2, x_11);
 x_13 = lean::alloc_cnstr(1, 1, 0);
 lean::cnstr_set(x_13, 0, x_12);
-x_14 = lean::alloc_cnstr(2, 2, 0);
-lean::cnstr_set(x_14, 0, x_13);
-lean::cnstr_set(x_14, 1, x_8);
-x_15 = lean::mk_nat_obj(1u);
-x_16 = lean::mk_array(x_15, x_14);
-x_17 = lean::box(0);
-x_18 = lean::alloc_cnstr(1, 3, 0);
-lean::cnstr_set(x_18, 0, x_1);
-lean::cnstr_set(x_18, 1, x_16);
-lean::cnstr_set(x_18, 2, x_17);
-x_19 = l_Lean_Parser_ParserState_pushSyntax(x_9, x_18);
-return x_19;
+x_14 = l_Lean_mkLit(x_1, x_8, x_13);
+x_15 = l_Lean_Parser_ParserState_pushSyntax(x_9, x_14);
+return x_15;
 }
 }
 obj* l_Lean_Parser_mkNodeToken___boxed(obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
@@ -4539,7 +4510,7 @@ return x_15;
 else
 {
 obj* x_18; obj* x_19; 
-x_18 = l_Lean_Parser_strLitKind;
+x_18 = l_Lean_strLitKind;
 x_19 = l_Lean_Parser_mkNodeToken(x_18, x_1, x_2, x_9);
 return x_19;
 }
@@ -4638,7 +4609,7 @@ if (x_9 == 0)
 {
 obj* x_10; obj* x_11; 
 lean::dec(x_6);
-x_10 = l_Lean_Parser_numLitKind;
+x_10 = l_Lean_numLitKind;
 x_11 = l_Lean_Parser_mkNodeToken(x_10, x_1, x_2, x_4);
 return x_11;
 }
@@ -4653,7 +4624,7 @@ if (x_14 == 0)
 {
 obj* x_15; obj* x_16; 
 lean::dec(x_12);
-x_15 = l_Lean_Parser_numLitKind;
+x_15 = l_Lean_numLitKind;
 x_16 = l_Lean_Parser_mkNodeToken(x_15, x_1, x_2, x_4);
 return x_16;
 }
@@ -4662,7 +4633,7 @@ else
 obj* x_17; obj* x_18; obj* x_19; obj* x_20; 
 x_17 = l_Lean_Parser_ParserState_setPos(x_4, x_12);
 x_18 = l_Lean_Parser_takeUntilFn___main___at_Lean_Parser_decimalNumberFn___spec__2(x_2, x_17);
-x_19 = l_Lean_Parser_numLitKind;
+x_19 = l_Lean_numLitKind;
 x_20 = l_Lean_Parser_mkNodeToken(x_19, x_1, x_2, x_18);
 return x_20;
 }
@@ -4828,7 +4799,7 @@ if (lean::obj_tag(x_6) == 0)
 {
 obj* x_7; obj* x_8; obj* x_9; 
 x_7 = l_Lean_Parser_takeUntilFn___main___at_Lean_Parser_binNumberFn___spec__3(x_2, x_5);
-x_8 = l_Lean_Parser_numLitKind;
+x_8 = l_Lean_numLitKind;
 x_9 = l_Lean_Parser_mkNodeToken(x_8, x_1, x_2, x_7);
 return x_9;
 }
@@ -4836,7 +4807,7 @@ else
 {
 obj* x_10; obj* x_11; 
 lean::dec(x_6);
-x_10 = l_Lean_Parser_numLitKind;
+x_10 = l_Lean_numLitKind;
 x_11 = l_Lean_Parser_mkNodeToken(x_10, x_1, x_2, x_5);
 return x_11;
 }
@@ -5006,7 +4977,7 @@ if (lean::obj_tag(x_6) == 0)
 {
 obj* x_7; obj* x_8; obj* x_9; 
 x_7 = l_Lean_Parser_takeUntilFn___main___at_Lean_Parser_octalNumberFn___spec__3(x_2, x_5);
-x_8 = l_Lean_Parser_numLitKind;
+x_8 = l_Lean_numLitKind;
 x_9 = l_Lean_Parser_mkNodeToken(x_8, x_1, x_2, x_7);
 return x_9;
 }
@@ -5014,7 +4985,7 @@ else
 {
 obj* x_10; obj* x_11; 
 lean::dec(x_6);
-x_10 = l_Lean_Parser_numLitKind;
+x_10 = l_Lean_numLitKind;
 x_11 = l_Lean_Parser_mkNodeToken(x_10, x_1, x_2, x_5);
 return x_11;
 }
@@ -5374,7 +5345,7 @@ if (lean::obj_tag(x_6) == 0)
 {
 obj* x_7; obj* x_8; obj* x_9; 
 x_7 = l_Lean_Parser_takeUntilFn___main___at_Lean_Parser_hexNumberFn___spec__3(x_2, x_5);
-x_8 = l_Lean_Parser_numLitKind;
+x_8 = l_Lean_numLitKind;
 x_9 = l_Lean_Parser_mkNodeToken(x_8, x_1, x_2, x_7);
 return x_9;
 }
@@ -5382,7 +5353,7 @@ else
 {
 obj* x_10; obj* x_11; 
 lean::dec(x_6);
-x_10 = l_Lean_Parser_numLitKind;
+x_10 = l_Lean_numLitKind;
 x_11 = l_Lean_Parser_mkNodeToken(x_10, x_1, x_2, x_5);
 return x_11;
 }
@@ -7074,7 +7045,7 @@ x_5 = lean::cnstr_get(x_3, 0);
 lean::inc(x_5);
 x_6 = l_Array_back___at___private_init_lean_parser_parser_5__updateCache___spec__1(x_5);
 lean::dec(x_5);
-x_7 = l_Lean_Parser_numLitKind;
+x_7 = l_Lean_numLitKind;
 x_8 = l_Lean_Syntax_isOfKind___main(x_6, x_7);
 lean::dec(x_6);
 if (x_8 == 0)
@@ -7173,7 +7144,7 @@ x_5 = lean::cnstr_get(x_3, 0);
 lean::inc(x_5);
 x_6 = l_Array_back___at___private_init_lean_parser_parser_5__updateCache___spec__1(x_5);
 lean::dec(x_5);
-x_7 = l_Lean_Parser_strLitKind;
+x_7 = l_Lean_strLitKind;
 x_8 = l_Lean_Syntax_isOfKind___main(x_6, x_7);
 lean::dec(x_6);
 if (x_8 == 0)
@@ -18295,12 +18266,12 @@ lean::dec(x_19);
 x_20 = lean::cnstr_get(x_11, 0);
 lean::inc(x_20);
 lean::dec(x_11);
-x_21 = l_Lean_Parser_numLitKind;
+x_21 = l_Lean_numLitKind;
 x_22 = lean_name_dec_eq(x_20, x_21);
 if (x_22 == 0)
 {
 obj* x_23; uint8 x_24; 
-x_23 = l_Lean_Parser_strLitKind;
+x_23 = l_Lean_strLitKind;
 x_24 = lean_name_dec_eq(x_20, x_23);
 lean::dec(x_20);
 if (x_24 == 0)
@@ -18336,12 +18307,12 @@ lean::dec(x_3);
 x_29 = lean::cnstr_get(x_11, 0);
 lean::inc(x_29);
 lean::dec(x_11);
-x_30 = l_Lean_Parser_numLitKind;
+x_30 = l_Lean_numLitKind;
 x_31 = lean_name_dec_eq(x_29, x_30);
 if (x_31 == 0)
 {
 obj* x_32; uint8 x_33; 
-x_32 = l_Lean_Parser_strLitKind;
+x_32 = l_Lean_strLitKind;
 x_33 = lean_name_dec_eq(x_29, x_32);
 lean::dec(x_29);
 if (x_33 == 0)
@@ -22036,12 +22007,6 @@ REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name(lean::mk_const_na
 l_Lean_Parser_quotedCharFn___main___closed__1 = _init_l_Lean_Parser_quotedCharFn___main___closed__1();
 lean::mark_persistent(l_Lean_Parser_quotedCharFn___main___closed__1);
 REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "Parser"), "quotedCharFn"), 2, l_Lean_Parser_quotedCharFn___boxed);
-l_Lean_Parser_strLitKind = _init_l_Lean_Parser_strLitKind();
-lean::mark_persistent(l_Lean_Parser_strLitKind);
-lean::register_constant(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "Parser"), "strLitKind"), l_Lean_Parser_strLitKind);
-l_Lean_Parser_numLitKind = _init_l_Lean_Parser_numLitKind();
-lean::mark_persistent(l_Lean_Parser_numLitKind);
-lean::register_constant(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "Parser"), "numLitKind"), l_Lean_Parser_numLitKind);
 REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "Parser"), "mkNodeToken"), 4, l_Lean_Parser_mkNodeToken___boxed);
 REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "Parser"), "strLitFnAux"), 3, l_Lean_Parser_strLitFnAux___boxed);
 REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "Parser"), "decimalNumberFn"), 3, l_Lean_Parser_decimalNumberFn___boxed);
diff --git a/src/stage0/init/lean/syntax.cpp b/src/stage0/init/lean/syntax.cpp
index f366c004c6..2a3917654b 100644
--- a/src/stage0/init/lean/syntax.cpp
+++ b/src/stage0/init/lean/syntax.cpp
@@ -14,6 +14,7 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64;
 #pragma GCC diagnostic ignored "-Wunused-label"
 #pragma GCC diagnostic ignored "-Wunused-but-set-variable"
 #endif
+obj* l___private_init_lean_syntax_5__decodeOctalLitAux___main(obj*, obj*, obj*);
 obj* l_unsafeCast(obj*, obj*, obj*, obj*);
 obj* l_Lean_Syntax_getHeadInfo___boxed(obj*);
 obj* l_Lean_Syntax_replace(obj*, obj*, obj*);
@@ -21,31 +22,35 @@ obj* l_Array_miterateAux___main___at_Lean_Syntax_reprint___main___spec__1(obj*,
 extern "C" uint8 lean_name_dec_eq(obj*, obj*);
 obj* l_Lean_Syntax_reprint___main___boxed(obj*);
 obj* l_Lean_Syntax_flipScopes___rarg(obj*);
+obj* l_Lean_Syntax_isNatLit(obj*);
 extern obj* l_Array_empty___closed__1;
 namespace lean {
 obj* nat_sub(obj*, obj*);
 }
 obj* l_Lean_stxInh;
 obj* l_Lean_Syntax_mreplace___main___at_Lean_Syntax_replace___spec__1(obj*, obj*);
-namespace lean {
-obj* mk_syntax_atom_core(obj*);
-}
 extern obj* l_Lean_Format_paren___closed__2;
 obj* l_Lean_Syntax_formatStx___main___closed__5;
 obj* l_Lean_Syntax_isOfKind___boxed(obj*, obj*);
+obj* l_Array_mkArray(obj*, obj*, obj*);
 obj* l_Lean_withArgs___rarg(obj*, obj*);
 obj* l_Lean_Syntax_toSyntaxNode(obj*);
 obj* l_Array_ummapAux___main___at_Lean_Syntax_updateLeading___spec__2(obj*, obj*, obj*);
+obj* l___private_init_lean_syntax_5__decodeOctalLitAux___main___boxed(obj*, obj*, obj*);
 obj* l_Lean_Format_group___main(obj*);
 obj* l___private_init_lean_syntax_3__reprintLeaf___main___boxed(obj*, obj*);
+obj* l___private_init_lean_syntax_5__decodeOctalLitAux(obj*, obj*, obj*);
 obj* l_Array_ummapAux___main___at_Lean_Syntax_mreplace___main___spec__1(obj*);
 obj* l___private_init_lean_syntax_3__reprintLeaf(obj*, obj*);
+obj* l_Lean_mkStrLit(obj*, obj*);
 obj* l_Lean_Syntax_replace___boxed(obj*, obj*, obj*);
 obj* l_Function_comp___rarg(obj*, obj*, obj*);
 obj* l_Lean_Syntax_reprint___main(obj*);
 obj* l_Array_ummapAux___main___at_Lean_Syntax_toSyntaxNode___spec__1(obj*, obj*);
 obj* l_List_reverse___rarg(obj*);
+obj* l___private_init_lean_syntax_4__decodeBinLitAux___main(obj*, obj*, obj*);
 obj* l_Lean_Syntax_formatStx___main(obj*);
+obj* l_Lean_numLitKind;
 obj* l_Lean_Format_joinSep___main___at_Lean_Syntax_formatStx___main___spec__2(obj*, obj*);
 uint8 l_Lean_Syntax_isOfKind___main(obj*, obj*);
 obj* l_Lean_Syntax_updateTrailing(obj*, obj*);
@@ -53,27 +58,35 @@ obj* l_Lean_updateArgs(obj*, obj*);
 obj* l_Lean_MacroScopes_flip(obj*, obj*);
 obj* l_Lean_Name_toStringWithSep___main(obj*, obj*);
 obj* l___private_init_lean_syntax_2__updateLeadingAux___main(obj*, obj*);
+obj* l___private_init_lean_syntax_5__decodeOctalLitAux___boxed(obj*, obj*, obj*);
 obj* l_Lean_Syntax_updateTrailing___main(obj*, obj*);
 extern obj* l_Lean_Format_sbracket___closed__1;
 obj* l_Lean_Syntax_isIdent___main___boxed(obj*);
 obj* l_Lean_Syntax_isMissing___main___boxed(obj*);
 obj* l_Lean_Syntax_reprint___boxed(obj*);
+obj* l___private_init_lean_syntax_8__decodeNatLitVal(obj*);
 obj* l_Lean_Syntax_formatStx___main___closed__2;
 obj* l_Lean_Syntax_flipScopes___main(obj*);
 obj* l_Lean_Syntax_HasToString;
 obj* l_Lean_Syntax_formatStx___main___closed__4;
+obj* l___private_init_lean_syntax_7__decodeDecimalLitAux___boxed(obj*, obj*, obj*);
 obj* l_Nat_decEq___boxed(obj*, obj*);
 obj* l_Array_miterateAux___main___at_Lean_Syntax_reprint___main___spec__2(obj*, obj*, obj*, obj*);
+obj* l___private_init_lean_syntax_6__decodeHexLitAux(obj*, obj*, obj*);
+obj* l_Lean_mkNumLit(obj*, obj*);
 extern obj* l_Lean_Format_join___closed__1;
+obj* l___private_init_lean_syntax_6__decodeHexLitAux___main___boxed(obj*, obj*, obj*);
 obj* l_Lean_SourceInfo_updateTrailing(obj*, obj*);
 obj* l___private_init_lean_syntax_1__updateInfo___main(obj*, obj*);
 obj* l_Array_toList___rarg(obj*);
 obj* l_Lean_Syntax_replace___rarg(obj*, obj*);
 obj* l_List_map___main___at_Lean_Syntax_formatStx___main___spec__4(obj*);
 obj* l_Nat_repr(obj*);
+obj* l___private_init_lean_syntax_4__decodeBinLitAux___main___boxed(obj*, obj*, obj*);
 obj* l_Lean_Syntax_mreplace___main___rarg___lambda__3(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 extern obj* l_Lean_Format_sbracket___closed__2;
 obj* l_Lean_Syntax_isMissing___boxed(obj*);
+obj* l_Lean_Syntax_isStrLit___main(obj*);
 obj* l_Lean_Syntax_mreplace___main___rarg(obj*, obj*, obj*);
 obj* l_Lean_Syntax_reprint___main___closed__1;
 obj* l_Lean_Syntax_mreplace___boxed(obj*);
@@ -81,15 +94,23 @@ obj* l_Lean_unreachIsNodeIdent___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*)
 obj* l_Lean_MacroScope_DecidableEq;
 obj* l_List_map___main___at_Lean_Syntax_formatStx___main___spec__1(obj*);
 obj* l_Lean_Syntax_getPos___boxed(obj*);
+obj* l_Lean_Syntax_isNatLit___main(obj*);
 obj* l_Array_miterateAux___main___at_Lean_Syntax_reprint___main___spec__1___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_Syntax_Lean_HasFormat;
 obj* l_Lean_Syntax_formatStx(obj*);
 namespace lean {
+obj* mk_syntax_str_lit_core(obj*);
+}
+namespace lean {
 obj* string_append(obj*, obj*);
 }
 obj* l_Array_mfindAux___main___at_Lean_Syntax_getHeadInfo___main___spec__1___boxed(obj*, obj*);
+uint8 l_UInt32_decLe(uint32, uint32);
 obj* l___private_init_lean_syntax_2__updateLeadingAux(obj*, obj*);
 extern obj* l_Lean_Format_paren___closed__1;
+namespace lean {
+uint8 string_utf8_at_end(obj*, obj*);
+}
 obj* l_Lean_Syntax_mreplace___main___at_Lean_Syntax_updateLeading___spec__1(obj*, obj*);
 uint8 l_Lean_Syntax_isOfKind(obj*, obj*);
 obj* l_Lean_Syntax_getHeadInfo___main(obj*);
@@ -117,37 +138,59 @@ namespace lean {
 uint8 nat_dec_eq(obj*, obj*);
 }
 obj* l_Lean_Syntax_mreplace___main___rarg___lambda__1(obj*, obj*, obj*);
+namespace lean {
+obj* mk_syntax_ident_core(obj*);
+}
+obj* l_Lean_strLitKind;
+obj* l_Lean_Syntax_isStrLit___main___boxed(obj*);
 obj* l_List_map___main___at_Lean_Syntax_formatStx___main___spec__5(obj*);
 obj* l_Lean_Syntax_reprint(obj*);
 obj* l_Lean_Syntax_getHeadInfo(obj*);
+namespace lean {
+uint32 string_utf8_get(obj*, obj*);
+}
 obj* l_Lean_Syntax_mreplace___rarg(obj*, obj*, obj*);
 obj* l_Lean_unreachIsNodeMissing(obj*, obj*);
 namespace lean {
 uint8 string_dec_eq(obj*, obj*);
 }
 obj* l_Lean_HasRepr___lambda__1(obj*);
+uint8 l_UInt32_decEq(uint32, uint32);
 uint8 l_Lean_Syntax_isIdent(obj*);
 obj* l_Array_mfindAux___main___at_Lean_Syntax_getHeadInfo___main___spec__1(obj*, obj*);
 obj* l_Lean_Syntax_updateLeading(obj*);
 obj* l_Lean_Format_joinSep___main___at_Lean_Syntax_formatStx___main___spec__2___boxed(obj*, obj*);
 obj* l___private_init_lean_syntax_1__updateInfo(obj*, obj*);
+uint8 l_Char_isDigit(uint32);
 obj* l_Lean_Syntax_flipScopes(obj*);
+obj* l___private_init_lean_syntax_8__decodeNatLitVal___closed__1;
 obj* l_Lean_Name_replacePrefix___main(obj*, obj*, obj*);
 extern obj* l_Lean_Format_sbracket___closed__3;
+obj* l___private_init_lean_syntax_6__decodeHexLitAux___main(obj*, obj*, obj*);
 obj* l_Lean_MacroScope_Lean_HasFormat;
 extern obj* l_Lean_formatKVMap___closed__1;
+namespace lean {
+obj* mk_syntax_list_core(obj*);
+}
+obj* l_Lean_Syntax_isNatLit___main___boxed(obj*);
+obj* l_Lean_Syntax_isStrLit(obj*);
 obj* l_Lean_Syntax_flipScopes___boxed(obj*);
+namespace lean {
+obj* mk_syntax_num_lit_core(obj*);
+}
 obj* l_Lean_Syntax_getPos(obj*);
 obj* l_Array_size(obj*, obj*);
 obj* l_Array_fset(obj*, obj*, obj*, obj*);
 obj* l_Array_get(obj*, obj*, obj*, obj*);
-namespace lean {
-obj* mk_syntax_list_core(obj*);
-}
 obj* l___private_init_lean_syntax_3__reprintLeaf___boxed(obj*, obj*);
+obj* l___private_init_lean_syntax_7__decodeDecimalLitAux___main___boxed(obj*, obj*, obj*);
 obj* l_Lean_Format_joinSep___main___at_Lean_Syntax_formatStx___main___spec__3(obj*, obj*);
 obj* l_Array_ummapAux___main___at_Lean_Syntax_mreplace___main___spec__1___rarg(obj*, obj*, obj*, obj*);
 obj* l_Lean_unreachIsNodeAtom___boxed(obj*, obj*, obj*, obj*);
+obj* l___private_init_lean_syntax_7__decodeDecimalLitAux___main(obj*, obj*, obj*);
+namespace lean {
+obj* string_utf8_next(obj*, obj*);
+}
 obj* l_Array_ummapAux___main___at_Lean_Syntax_mreplace___main___spec__1___rarg___lambda__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
 extern obj* l_Lean_formatDataValue___main___closed__3;
 obj* l_Array_ummapAux___main___at_Lean_Syntax_mreplace___main___spec__1___boxed(obj*);
@@ -155,29 +198,43 @@ extern obj* l_Lean_Name_toString___closed__1;
 namespace lean {
 obj* string_utf8_extract(obj*, obj*, obj*);
 }
+obj* l___private_init_lean_syntax_4__decodeBinLitAux___boxed(obj*, obj*, obj*);
 obj* l_Lean_Syntax_isOfKind___main___boxed(obj*, obj*);
 namespace lean {
 obj* string_utf8_byte_size(obj*);
 }
+obj* l_Lean_Syntax_isNatLit___boxed(obj*);
+obj* l___private_init_lean_syntax_8__decodeNatLitVal___boxed(obj*);
+namespace lean {
+obj* uint32_to_nat(uint32);
+}
+obj* l___private_init_lean_syntax_4__decodeBinLitAux(obj*, obj*, obj*);
 obj* l_Lean_Syntax_mreplace___main___boxed(obj*);
 obj* l_Array_set(obj*, obj*, obj*, obj*);
 obj* l___private_init_lean_syntax_3__reprintLeaf___main(obj*, obj*);
 obj* l_Lean_MacroScopes_flip___main(obj*, obj*);
+obj* l___private_init_lean_syntax_7__decodeDecimalLitAux(obj*, obj*, obj*);
 obj* l_Lean_Syntax_formatStx___main___closed__6;
 obj* l_String_quote(obj*);
 obj* l_Lean_Syntax_mreplace(obj*);
+obj* l_Lean_Syntax_isStrLit___boxed(obj*);
+namespace lean {
+obj* mk_syntax_atom_core(obj*);
+}
 obj* l_Lean_Syntax_mreplace___main(obj*);
 obj* l_Array_miterateAux___main___at_Lean_Syntax_reprint___main___spec__2___boxed(obj*, obj*, obj*, obj*);
+obj* l_Lean_mkLit(obj*, obj*, obj*);
+namespace lean {
+obj* nat_mul(obj*, obj*);
+}
 obj* l_Lean_withArgs(obj*);
 obj* l_Lean_MacroScopes_flip___boxed(obj*, obj*);
+obj* l___private_init_lean_syntax_6__decodeHexLitAux___boxed(obj*, obj*, obj*);
 obj* l_Array_ummapAux___main___at_Lean_Syntax_replace___spec__2(obj*, obj*, obj*);
 obj* l_Lean_Syntax_toSyntaxNode___rarg(obj*, obj*, obj*);
 obj* l_Lean_Syntax_isIdent___boxed(obj*);
 obj* l_Lean_Syntax_getHeadInfo___main___boxed(obj*);
 obj* l_Lean_SourceInfo_updateTrailing___main(obj*, obj*);
-namespace lean {
-obj* mk_syntax_ident_core(obj*);
-}
 obj* l_Lean_Syntax_toSyntaxNode___rarg___boxed(obj*, obj*, obj*);
 obj* l_Lean_unreachIsNodeIdent(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 uint8 l_Lean_Syntax_isMissing(obj*);
@@ -259,6 +316,26 @@ x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
+obj* _init_l_Lean_strLitKind() {
+_start:
+{
+obj* x_1; obj* x_2; obj* x_3; 
+x_1 = lean::box(0);
+x_2 = lean::mk_string("strLit");
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+obj* _init_l_Lean_numLitKind() {
+_start:
+{
+obj* x_1; obj* x_2; obj* x_3; 
+x_1 = lean::box(0);
+x_2 = lean::mk_string("numLit");
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
 obj* _init_l_Lean_stxInh() {
 _start:
 {
@@ -3457,6 +3534,919 @@ return x_4;
 }
 }
 }
+obj* l_Lean_mkLit(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; 
+x_4 = lean::alloc_cnstr(2, 2, 0);
+lean::cnstr_set(x_4, 0, x_3);
+lean::cnstr_set(x_4, 1, x_2);
+x_5 = lean::mk_nat_obj(1u);
+x_6 = lean::mk_array(x_5, x_4);
+x_7 = lean::box(0);
+x_8 = lean::alloc_cnstr(1, 3, 0);
+lean::cnstr_set(x_8, 0, x_1);
+lean::cnstr_set(x_8, 1, x_6);
+lean::cnstr_set(x_8, 2, x_7);
+return x_8;
+}
+}
+obj* l_Lean_mkStrLit(obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; obj* x_4; 
+x_3 = l_Lean_strLitKind;
+x_4 = l_Lean_mkLit(x_3, x_1, x_2);
+return x_4;
+}
+}
+obj* l_Lean_mkNumLit(obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; obj* x_4; 
+x_3 = l_Lean_numLitKind;
+x_4 = l_Lean_mkLit(x_3, x_1, x_2);
+return x_4;
+}
+}
+namespace lean {
+obj* mk_syntax_str_lit_core(obj* x_1) {
+_start:
+{
+obj* x_2; obj* x_3; obj* x_4; 
+x_2 = lean::box(0);
+x_3 = l_Lean_strLitKind;
+x_4 = l_Lean_mkLit(x_3, x_1, x_2);
+return x_4;
+}
+}
+}
+namespace lean {
+obj* mk_syntax_num_lit_core(obj* x_1) {
+_start:
+{
+obj* x_2; obj* x_3; obj* x_4; obj* x_5; 
+x_2 = l_Nat_repr(x_1);
+x_3 = lean::box(0);
+x_4 = l_Lean_numLitKind;
+x_5 = l_Lean_mkLit(x_4, x_2, x_3);
+return x_5;
+}
+}
+}
+obj* l_Lean_Syntax_isStrLit___main(obj* x_1) {
+_start:
+{
+if (lean::obj_tag(x_1) == 1)
+{
+obj* x_2; obj* x_3; obj* x_4; uint8 x_5; 
+x_2 = lean::cnstr_get(x_1, 0);
+x_3 = lean::cnstr_get(x_1, 1);
+x_4 = l_Lean_strLitKind;
+x_5 = lean_name_dec_eq(x_2, x_4);
+if (x_5 == 0)
+{
+obj* x_6; 
+x_6 = lean::box(0);
+return x_6;
+}
+else
+{
+obj* x_7; obj* x_8; uint8 x_9; 
+x_7 = lean::array_get_size(x_3);
+x_8 = lean::mk_nat_obj(1u);
+x_9 = lean::nat_dec_eq(x_7, x_8);
+lean::dec(x_7);
+if (x_9 == 0)
+{
+obj* x_10; 
+x_10 = lean::box(0);
+return x_10;
+}
+else
+{
+obj* x_11; obj* x_12; obj* x_13; 
+x_11 = l_Lean_stxInh;
+x_12 = lean::mk_nat_obj(0u);
+x_13 = lean::array_get(x_11, x_3, x_12);
+if (lean::obj_tag(x_13) == 2)
+{
+obj* x_14; obj* x_15; 
+x_14 = lean::cnstr_get(x_13, 1);
+lean::inc(x_14);
+lean::dec(x_13);
+x_15 = lean::alloc_cnstr(1, 1, 0);
+lean::cnstr_set(x_15, 0, x_14);
+return x_15;
+}
+else
+{
+obj* x_16; 
+lean::dec(x_13);
+x_16 = lean::box(0);
+return x_16;
+}
+}
+}
+}
+else
+{
+obj* x_17; 
+x_17 = lean::box(0);
+return x_17;
+}
+}
+}
+obj* l_Lean_Syntax_isStrLit___main___boxed(obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = l_Lean_Syntax_isStrLit___main(x_1);
+lean::dec(x_1);
+return x_2;
+}
+}
+obj* l_Lean_Syntax_isStrLit(obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = l_Lean_Syntax_isStrLit___main(x_1);
+return x_2;
+}
+}
+obj* l_Lean_Syntax_isStrLit___boxed(obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = l_Lean_Syntax_isStrLit(x_1);
+lean::dec(x_1);
+return x_2;
+}
+}
+obj* l___private_init_lean_syntax_4__decodeBinLitAux___main(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+uint8 x_4; 
+x_4 = lean::string_utf8_at_end(x_1, x_2);
+if (x_4 == 0)
+{
+uint32 x_5; uint32 x_6; uint8 x_7; 
+x_5 = lean::string_utf8_get(x_1, x_2);
+x_6 = 48;
+x_7 = x_5 == x_6;
+if (x_7 == 0)
+{
+uint32 x_8; uint8 x_9; 
+x_8 = 49;
+x_9 = x_5 == x_8;
+if (x_9 == 0)
+{
+obj* x_10; 
+lean::dec(x_3);
+lean::dec(x_2);
+x_10 = lean::box(0);
+return x_10;
+}
+else
+{
+obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_15; 
+x_11 = lean::string_utf8_next(x_1, x_2);
+lean::dec(x_2);
+x_12 = lean::mk_nat_obj(2u);
+x_13 = lean::nat_mul(x_12, x_3);
+lean::dec(x_3);
+x_14 = lean::mk_nat_obj(1u);
+x_15 = lean::nat_add(x_13, x_14);
+lean::dec(x_13);
+x_2 = x_11;
+x_3 = x_15;
+goto _start;
+}
+}
+else
+{
+obj* x_17; obj* x_18; obj* x_19; 
+x_17 = lean::string_utf8_next(x_1, x_2);
+lean::dec(x_2);
+x_18 = lean::mk_nat_obj(2u);
+x_19 = lean::nat_mul(x_18, x_3);
+lean::dec(x_3);
+x_2 = x_17;
+x_3 = x_19;
+goto _start;
+}
+}
+else
+{
+obj* x_21; 
+lean::dec(x_2);
+x_21 = lean::alloc_cnstr(1, 1, 0);
+lean::cnstr_set(x_21, 0, x_3);
+return x_21;
+}
+}
+}
+obj* l___private_init_lean_syntax_4__decodeBinLitAux___main___boxed(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = l___private_init_lean_syntax_4__decodeBinLitAux___main(x_1, x_2, x_3);
+lean::dec(x_1);
+return x_4;
+}
+}
+obj* l___private_init_lean_syntax_4__decodeBinLitAux(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = l___private_init_lean_syntax_4__decodeBinLitAux___main(x_1, x_2, x_3);
+return x_4;
+}
+}
+obj* l___private_init_lean_syntax_4__decodeBinLitAux___boxed(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = l___private_init_lean_syntax_4__decodeBinLitAux(x_1, x_2, x_3);
+lean::dec(x_1);
+return x_4;
+}
+}
+obj* l___private_init_lean_syntax_5__decodeOctalLitAux___main(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+uint8 x_4; 
+x_4 = lean::string_utf8_at_end(x_1, x_2);
+if (x_4 == 0)
+{
+uint32 x_5; uint32 x_6; uint8 x_7; 
+x_5 = lean::string_utf8_get(x_1, x_2);
+x_6 = 48;
+x_7 = x_6 <= x_5;
+if (x_7 == 0)
+{
+obj* x_8; 
+lean::dec(x_3);
+lean::dec(x_2);
+x_8 = lean::box(0);
+return x_8;
+}
+else
+{
+uint32 x_9; uint8 x_10; 
+x_9 = 55;
+x_10 = x_5 <= x_9;
+if (x_10 == 0)
+{
+obj* x_11; 
+lean::dec(x_3);
+lean::dec(x_2);
+x_11 = lean::box(0);
+return x_11;
+}
+else
+{
+obj* x_12; obj* x_13; obj* x_14; obj* x_15; obj* x_16; obj* x_17; obj* x_18; 
+x_12 = lean::string_utf8_next(x_1, x_2);
+lean::dec(x_2);
+x_13 = lean::mk_nat_obj(8u);
+x_14 = lean::nat_mul(x_13, x_3);
+lean::dec(x_3);
+x_15 = lean::uint32_to_nat(x_5);
+x_16 = lean::nat_add(x_14, x_15);
+lean::dec(x_15);
+lean::dec(x_14);
+x_17 = lean::mk_nat_obj(48u);
+x_18 = lean::nat_sub(x_16, x_17);
+lean::dec(x_16);
+x_2 = x_12;
+x_3 = x_18;
+goto _start;
+}
+}
+}
+else
+{
+obj* x_20; 
+lean::dec(x_2);
+x_20 = lean::alloc_cnstr(1, 1, 0);
+lean::cnstr_set(x_20, 0, x_3);
+return x_20;
+}
+}
+}
+obj* l___private_init_lean_syntax_5__decodeOctalLitAux___main___boxed(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = l___private_init_lean_syntax_5__decodeOctalLitAux___main(x_1, x_2, x_3);
+lean::dec(x_1);
+return x_4;
+}
+}
+obj* l___private_init_lean_syntax_5__decodeOctalLitAux(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = l___private_init_lean_syntax_5__decodeOctalLitAux___main(x_1, x_2, x_3);
+return x_4;
+}
+}
+obj* l___private_init_lean_syntax_5__decodeOctalLitAux___boxed(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = l___private_init_lean_syntax_5__decodeOctalLitAux(x_1, x_2, x_3);
+lean::dec(x_1);
+return x_4;
+}
+}
+obj* l___private_init_lean_syntax_6__decodeHexLitAux___main(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+uint8 x_4; 
+x_4 = lean::string_utf8_at_end(x_1, x_2);
+if (x_4 == 0)
+{
+uint32 x_5; obj* x_6; uint32 x_54; uint8 x_55; 
+x_5 = lean::string_utf8_get(x_1, x_2);
+x_54 = 48;
+x_55 = x_54 <= x_5;
+if (x_55 == 0)
+{
+obj* x_56; 
+x_56 = lean::box(0);
+x_6 = x_56;
+goto block_53;
+}
+else
+{
+uint32 x_57; uint8 x_58; 
+x_57 = 57;
+x_58 = x_5 <= x_57;
+if (x_58 == 0)
+{
+obj* x_59; 
+x_59 = lean::box(0);
+x_6 = x_59;
+goto block_53;
+}
+else
+{
+obj* x_60; obj* x_61; obj* x_62; obj* x_63; obj* x_64; obj* x_65; obj* x_66; 
+x_60 = lean::string_utf8_next(x_1, x_2);
+lean::dec(x_2);
+x_61 = lean::mk_nat_obj(16u);
+x_62 = lean::nat_mul(x_61, x_3);
+lean::dec(x_3);
+x_63 = lean::uint32_to_nat(x_5);
+x_64 = lean::nat_add(x_62, x_63);
+lean::dec(x_63);
+lean::dec(x_62);
+x_65 = lean::mk_nat_obj(48u);
+x_66 = lean::nat_sub(x_64, x_65);
+lean::dec(x_64);
+x_2 = x_60;
+x_3 = x_66;
+goto _start;
+}
+}
+block_53:
+{
+uint32 x_7; uint8 x_8; 
+lean::dec(x_6);
+x_7 = 97;
+x_8 = x_7 <= x_5;
+if (x_8 == 0)
+{
+uint32 x_9; uint8 x_10; 
+x_9 = 65;
+x_10 = x_9 <= x_5;
+if (x_10 == 0)
+{
+obj* x_11; 
+lean::dec(x_3);
+lean::dec(x_2);
+x_11 = lean::box(0);
+return x_11;
+}
+else
+{
+uint32 x_12; uint8 x_13; 
+x_12 = 70;
+x_13 = x_5 <= x_12;
+if (x_13 == 0)
+{
+obj* x_14; 
+lean::dec(x_3);
+lean::dec(x_2);
+x_14 = lean::box(0);
+return x_14;
+}
+else
+{
+obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_21; obj* x_22; obj* x_23; 
+x_15 = lean::string_utf8_next(x_1, x_2);
+lean::dec(x_2);
+x_16 = lean::mk_nat_obj(16u);
+x_17 = lean::nat_mul(x_16, x_3);
+lean::dec(x_3);
+x_18 = lean::mk_nat_obj(10u);
+x_19 = lean::nat_add(x_17, x_18);
+lean::dec(x_17);
+x_20 = lean::uint32_to_nat(x_5);
+x_21 = lean::nat_add(x_19, x_20);
+lean::dec(x_20);
+lean::dec(x_19);
+x_22 = lean::mk_nat_obj(65u);
+x_23 = lean::nat_sub(x_21, x_22);
+lean::dec(x_21);
+x_2 = x_15;
+x_3 = x_23;
+goto _start;
+}
+}
+}
+else
+{
+uint32 x_25; uint8 x_26; 
+x_25 = 102;
+x_26 = x_5 <= x_25;
+if (x_26 == 0)
+{
+uint32 x_27; uint8 x_28; 
+x_27 = 65;
+x_28 = x_27 <= x_5;
+if (x_28 == 0)
+{
+obj* x_29; 
+lean::dec(x_3);
+lean::dec(x_2);
+x_29 = lean::box(0);
+return x_29;
+}
+else
+{
+uint32 x_30; uint8 x_31; 
+x_30 = 70;
+x_31 = x_5 <= x_30;
+if (x_31 == 0)
+{
+obj* x_32; 
+lean::dec(x_3);
+lean::dec(x_2);
+x_32 = lean::box(0);
+return x_32;
+}
+else
+{
+obj* x_33; obj* x_34; obj* x_35; obj* x_36; obj* x_37; obj* x_38; obj* x_39; obj* x_40; obj* x_41; 
+x_33 = lean::string_utf8_next(x_1, x_2);
+lean::dec(x_2);
+x_34 = lean::mk_nat_obj(16u);
+x_35 = lean::nat_mul(x_34, x_3);
+lean::dec(x_3);
+x_36 = lean::mk_nat_obj(10u);
+x_37 = lean::nat_add(x_35, x_36);
+lean::dec(x_35);
+x_38 = lean::uint32_to_nat(x_5);
+x_39 = lean::nat_add(x_37, x_38);
+lean::dec(x_38);
+lean::dec(x_37);
+x_40 = lean::mk_nat_obj(65u);
+x_41 = lean::nat_sub(x_39, x_40);
+lean::dec(x_39);
+x_2 = x_33;
+x_3 = x_41;
+goto _start;
+}
+}
+}
+else
+{
+obj* x_43; obj* x_44; obj* x_45; obj* x_46; obj* x_47; obj* x_48; obj* x_49; obj* x_50; obj* x_51; 
+x_43 = lean::string_utf8_next(x_1, x_2);
+lean::dec(x_2);
+x_44 = lean::mk_nat_obj(16u);
+x_45 = lean::nat_mul(x_44, x_3);
+lean::dec(x_3);
+x_46 = lean::mk_nat_obj(10u);
+x_47 = lean::nat_add(x_45, x_46);
+lean::dec(x_45);
+x_48 = lean::uint32_to_nat(x_5);
+x_49 = lean::nat_add(x_47, x_48);
+lean::dec(x_48);
+lean::dec(x_47);
+x_50 = lean::mk_nat_obj(97u);
+x_51 = lean::nat_sub(x_49, x_50);
+lean::dec(x_49);
+x_2 = x_43;
+x_3 = x_51;
+goto _start;
+}
+}
+}
+}
+else
+{
+obj* x_68; 
+lean::dec(x_2);
+x_68 = lean::alloc_cnstr(1, 1, 0);
+lean::cnstr_set(x_68, 0, x_3);
+return x_68;
+}
+}
+}
+obj* l___private_init_lean_syntax_6__decodeHexLitAux___main___boxed(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = l___private_init_lean_syntax_6__decodeHexLitAux___main(x_1, x_2, x_3);
+lean::dec(x_1);
+return x_4;
+}
+}
+obj* l___private_init_lean_syntax_6__decodeHexLitAux(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = l___private_init_lean_syntax_6__decodeHexLitAux___main(x_1, x_2, x_3);
+return x_4;
+}
+}
+obj* l___private_init_lean_syntax_6__decodeHexLitAux___boxed(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = l___private_init_lean_syntax_6__decodeHexLitAux(x_1, x_2, x_3);
+lean::dec(x_1);
+return x_4;
+}
+}
+obj* l___private_init_lean_syntax_7__decodeDecimalLitAux___main(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+uint8 x_4; 
+x_4 = lean::string_utf8_at_end(x_1, x_2);
+if (x_4 == 0)
+{
+uint32 x_5; uint32 x_6; uint8 x_7; 
+x_5 = lean::string_utf8_get(x_1, x_2);
+x_6 = 48;
+x_7 = x_6 <= x_5;
+if (x_7 == 0)
+{
+obj* x_8; 
+lean::dec(x_3);
+lean::dec(x_2);
+x_8 = lean::box(0);
+return x_8;
+}
+else
+{
+uint32 x_9; uint8 x_10; 
+x_9 = 57;
+x_10 = x_5 <= x_9;
+if (x_10 == 0)
+{
+obj* x_11; 
+lean::dec(x_3);
+lean::dec(x_2);
+x_11 = lean::box(0);
+return x_11;
+}
+else
+{
+obj* x_12; obj* x_13; obj* x_14; obj* x_15; obj* x_16; obj* x_17; obj* x_18; 
+x_12 = lean::string_utf8_next(x_1, x_2);
+lean::dec(x_2);
+x_13 = lean::mk_nat_obj(10u);
+x_14 = lean::nat_mul(x_13, x_3);
+lean::dec(x_3);
+x_15 = lean::uint32_to_nat(x_5);
+x_16 = lean::nat_add(x_14, x_15);
+lean::dec(x_15);
+lean::dec(x_14);
+x_17 = lean::mk_nat_obj(48u);
+x_18 = lean::nat_sub(x_16, x_17);
+lean::dec(x_16);
+x_2 = x_12;
+x_3 = x_18;
+goto _start;
+}
+}
+}
+else
+{
+obj* x_20; 
+lean::dec(x_2);
+x_20 = lean::alloc_cnstr(1, 1, 0);
+lean::cnstr_set(x_20, 0, x_3);
+return x_20;
+}
+}
+}
+obj* l___private_init_lean_syntax_7__decodeDecimalLitAux___main___boxed(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = l___private_init_lean_syntax_7__decodeDecimalLitAux___main(x_1, x_2, x_3);
+lean::dec(x_1);
+return x_4;
+}
+}
+obj* l___private_init_lean_syntax_7__decodeDecimalLitAux(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = l___private_init_lean_syntax_7__decodeDecimalLitAux___main(x_1, x_2, x_3);
+return x_4;
+}
+}
+obj* l___private_init_lean_syntax_7__decodeDecimalLitAux___boxed(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = l___private_init_lean_syntax_7__decodeDecimalLitAux(x_1, x_2, x_3);
+lean::dec(x_1);
+return x_4;
+}
+}
+obj* _init_l___private_init_lean_syntax_8__decodeNatLitVal___closed__1() {
+_start:
+{
+obj* x_1; obj* x_2; 
+x_1 = lean::mk_nat_obj(0u);
+x_2 = lean::alloc_cnstr(1, 1, 0);
+lean::cnstr_set(x_2, 0, x_1);
+return x_2;
+}
+}
+obj* l___private_init_lean_syntax_8__decodeNatLitVal(obj* x_1) {
+_start:
+{
+obj* x_2; obj* x_3; uint8 x_4; 
+x_2 = lean::string_length(x_1);
+x_3 = lean::mk_nat_obj(0u);
+x_4 = lean::nat_dec_eq(x_2, x_3);
+if (x_4 == 0)
+{
+uint32 x_5; uint32 x_6; uint8 x_7; 
+x_5 = lean::string_utf8_get(x_1, x_3);
+x_6 = 48;
+x_7 = x_5 == x_6;
+if (x_7 == 0)
+{
+uint8 x_8; 
+lean::dec(x_2);
+x_8 = l_Char_isDigit(x_5);
+if (x_8 == 0)
+{
+obj* x_9; 
+x_9 = lean::box(0);
+return x_9;
+}
+else
+{
+obj* x_10; 
+x_10 = l___private_init_lean_syntax_7__decodeDecimalLitAux___main(x_1, x_3, x_3);
+return x_10;
+}
+}
+else
+{
+obj* x_11; uint8 x_12; 
+x_11 = lean::mk_nat_obj(1u);
+x_12 = lean::nat_dec_eq(x_2, x_11);
+lean::dec(x_2);
+if (x_12 == 0)
+{
+uint32 x_13; uint32 x_14; uint8 x_15; 
+x_13 = lean::string_utf8_get(x_1, x_11);
+x_14 = 120;
+x_15 = x_13 == x_14;
+if (x_15 == 0)
+{
+uint32 x_16; uint8 x_17; 
+x_16 = 88;
+x_17 = x_13 == x_16;
+if (x_17 == 0)
+{
+uint32 x_18; uint8 x_19; uint8 x_38; 
+x_18 = 98;
+x_38 = x_13 == x_18;
+if (x_38 == 0)
+{
+uint8 x_39; 
+x_39 = 0;
+x_19 = x_39;
+goto block_37;
+}
+else
+{
+uint8 x_40; 
+x_40 = 1;
+x_19 = x_40;
+goto block_37;
+}
+block_37:
+{
+if (x_19 == 0)
+{
+uint32 x_20; uint8 x_21; 
+x_20 = 66;
+x_21 = x_13 == x_20;
+if (x_21 == 0)
+{
+uint32 x_22; uint8 x_23; 
+x_22 = 111;
+x_23 = x_13 == x_22;
+if (x_23 == 0)
+{
+uint32 x_24; uint8 x_25; 
+x_24 = 79;
+x_25 = x_13 == x_24;
+if (x_25 == 0)
+{
+uint8 x_26; 
+x_26 = l_Char_isDigit(x_13);
+if (x_26 == 0)
+{
+obj* x_27; 
+x_27 = lean::box(0);
+return x_27;
+}
+else
+{
+obj* x_28; 
+x_28 = l___private_init_lean_syntax_7__decodeDecimalLitAux___main(x_1, x_3, x_3);
+return x_28;
+}
+}
+else
+{
+obj* x_29; obj* x_30; 
+x_29 = lean::mk_nat_obj(2u);
+x_30 = l___private_init_lean_syntax_5__decodeOctalLitAux___main(x_1, x_29, x_3);
+return x_30;
+}
+}
+else
+{
+obj* x_31; obj* x_32; 
+x_31 = lean::mk_nat_obj(2u);
+x_32 = l___private_init_lean_syntax_5__decodeOctalLitAux___main(x_1, x_31, x_3);
+return x_32;
+}
+}
+else
+{
+obj* x_33; obj* x_34; 
+x_33 = lean::mk_nat_obj(2u);
+x_34 = l___private_init_lean_syntax_4__decodeBinLitAux___main(x_1, x_33, x_3);
+return x_34;
+}
+}
+else
+{
+obj* x_35; obj* x_36; 
+x_35 = lean::mk_nat_obj(2u);
+x_36 = l___private_init_lean_syntax_4__decodeBinLitAux___main(x_1, x_35, x_3);
+return x_36;
+}
+}
+}
+else
+{
+obj* x_41; obj* x_42; 
+x_41 = lean::mk_nat_obj(2u);
+x_42 = l___private_init_lean_syntax_6__decodeHexLitAux___main(x_1, x_41, x_3);
+return x_42;
+}
+}
+else
+{
+obj* x_43; obj* x_44; 
+x_43 = lean::mk_nat_obj(2u);
+x_44 = l___private_init_lean_syntax_6__decodeHexLitAux___main(x_1, x_43, x_3);
+return x_44;
+}
+}
+else
+{
+obj* x_45; 
+x_45 = l___private_init_lean_syntax_8__decodeNatLitVal___closed__1;
+return x_45;
+}
+}
+}
+else
+{
+obj* x_46; 
+lean::dec(x_2);
+x_46 = lean::box(0);
+return x_46;
+}
+}
+}
+obj* l___private_init_lean_syntax_8__decodeNatLitVal___boxed(obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = l___private_init_lean_syntax_8__decodeNatLitVal(x_1);
+lean::dec(x_1);
+return x_2;
+}
+}
+obj* l_Lean_Syntax_isNatLit___main(obj* x_1) {
+_start:
+{
+if (lean::obj_tag(x_1) == 1)
+{
+obj* x_2; obj* x_3; obj* x_4; uint8 x_5; 
+x_2 = lean::cnstr_get(x_1, 0);
+x_3 = lean::cnstr_get(x_1, 1);
+x_4 = l_Lean_strLitKind;
+x_5 = lean_name_dec_eq(x_2, x_4);
+if (x_5 == 0)
+{
+obj* x_6; 
+x_6 = lean::box(0);
+return x_6;
+}
+else
+{
+obj* x_7; obj* x_8; uint8 x_9; 
+x_7 = lean::array_get_size(x_3);
+x_8 = lean::mk_nat_obj(1u);
+x_9 = lean::nat_dec_eq(x_7, x_8);
+lean::dec(x_7);
+if (x_9 == 0)
+{
+obj* x_10; 
+x_10 = lean::box(0);
+return x_10;
+}
+else
+{
+obj* x_11; obj* x_12; obj* x_13; 
+x_11 = l_Lean_stxInh;
+x_12 = lean::mk_nat_obj(0u);
+x_13 = lean::array_get(x_11, x_3, x_12);
+if (lean::obj_tag(x_13) == 2)
+{
+obj* x_14; obj* x_15; 
+x_14 = lean::cnstr_get(x_13, 1);
+lean::inc(x_14);
+lean::dec(x_13);
+x_15 = l___private_init_lean_syntax_8__decodeNatLitVal(x_14);
+lean::dec(x_14);
+return x_15;
+}
+else
+{
+obj* x_16; 
+lean::dec(x_13);
+x_16 = lean::box(0);
+return x_16;
+}
+}
+}
+}
+else
+{
+obj* x_17; 
+x_17 = lean::box(0);
+return x_17;
+}
+}
+}
+obj* l_Lean_Syntax_isNatLit___main___boxed(obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = l_Lean_Syntax_isNatLit___main(x_1);
+lean::dec(x_1);
+return x_2;
+}
+}
+obj* l_Lean_Syntax_isNatLit(obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = l_Lean_Syntax_isNatLit___main(x_1);
+return x_2;
+}
+}
+obj* l_Lean_Syntax_isNatLit___boxed(obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = l_Lean_Syntax_isNatLit(x_1);
+lean::dec(x_1);
+return x_2;
+}
+}
 obj* initialize_init_lean_name(obj*);
 obj* initialize_init_lean_format(obj*);
 obj* initialize_init_data_array_default(obj*);
@@ -3484,6 +4474,12 @@ lean::register_constant(lean::mk_const_name(lean::mk_const_name("Lean"), "choice
 l_Lean_nullKind = _init_l_Lean_nullKind();
 lean::mark_persistent(l_Lean_nullKind);
 lean::register_constant(lean::mk_const_name(lean::mk_const_name("Lean"), "nullKind"), l_Lean_nullKind);
+l_Lean_strLitKind = _init_l_Lean_strLitKind();
+lean::mark_persistent(l_Lean_strLitKind);
+lean::register_constant(lean::mk_const_name(lean::mk_const_name("Lean"), "strLitKind"), l_Lean_strLitKind);
+l_Lean_numLitKind = _init_l_Lean_numLitKind();
+lean::mark_persistent(l_Lean_numLitKind);
+lean::register_constant(lean::mk_const_name(lean::mk_const_name("Lean"), "numLitKind"), l_Lean_numLitKind);
 l_Lean_stxInh = _init_l_Lean_stxInh();
 lean::mark_persistent(l_Lean_stxInh);
 lean::register_constant(lean::mk_const_name(lean::mk_const_name("Lean"), "stxInh"), l_Lean_stxInh);
@@ -3526,8 +4522,17 @@ lean::register_constant(lean::mk_const_name(lean::mk_const_name(lean::mk_const_n
 l_Lean_Syntax_HasToString = _init_l_Lean_Syntax_HasToString();
 lean::mark_persistent(l_Lean_Syntax_HasToString);
 lean::register_constant(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "Syntax"), "HasToString"), l_Lean_Syntax_HasToString);
-REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "Syntax"), "mkSimpleAtom"), 1, lean::mk_syntax_atom_core);
-REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "Syntax"), "mkSimpleIdent"), 1, lean::mk_syntax_ident_core);
-REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "Syntax"), "mkListNode"), 1, lean::mk_syntax_list_core);
+REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "mkSimpleAtom"), 1, lean::mk_syntax_atom_core);
+REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "mkSimpleIdent"), 1, lean::mk_syntax_ident_core);
+REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "mkListNode"), 1, lean::mk_syntax_list_core);
+REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "mkLit"), 3, l_Lean_mkLit);
+REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "mkStrLit"), 2, l_Lean_mkStrLit);
+REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "mkNumLit"), 2, l_Lean_mkNumLit);
+REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "mkStrLitAux"), 1, lean::mk_syntax_str_lit_core);
+REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "mkNumLitAux"), 1, lean::mk_syntax_num_lit_core);
+REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "Syntax"), "isStrLit"), 1, l_Lean_Syntax_isStrLit___boxed);
+l___private_init_lean_syntax_8__decodeNatLitVal___closed__1 = _init_l___private_init_lean_syntax_8__decodeNatLitVal___closed__1();
+lean::mark_persistent(l___private_init_lean_syntax_8__decodeNatLitVal___closed__1);
+REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "Syntax"), "isNatLit"), 1, l_Lean_Syntax_isNatLit___boxed);
 return w;
 }