Parsing C-style octal number

Stream: lean4

[Yasu Watanabe]

I'm trying to be familiar with syntax extension method of Lean4. I gradually understand It's super flexible and really easy to implement new syntax in straight forward way from like EBNF.

I'm currently try to implement parsing mini language and have a problem parsing C-style octal number by the following code.

declare_syntax_cat oct  -- octal number
declare_syntax_cat oct1 -- leading 0 for octal number
declare_syntax_cat oct_digit -- octal digit one of [0,1,2,3,4,5,6,7]

syntax "0" : oct1
syntax "0" : oct_digit
syntax "1" : oct_digit
syntax "2" : oct_digit
syntax "3" : oct_digit
syntax "4" : oct_digit
syntax "5" : oct_digit
syntax "6" : oct_digit
syntax "7" : oct_digit
syntax "8" : oct_digit

syntax oct1 oct_digit+ : oct

Because 0 cannot be used as ident, I think the code above does not work.
Suggestion for this is very welcome.

[Mac]

Lean has a small set of core tokens (e.g., ident, num, char, str, scientific) that cannot be easily overwritten by user DSLs. To split them apart you must write a fully custom parser for the given piece of input. Alternatively, you could potentially just use the builtin num token as it supports octal numerals (in the form of 0o1234).