Reusing inbuilt syntax?

Stream: lean4

[Siddharth Bhat]

I'd like to overload the inbuilt true in a custom context of mine. As an MWE:

-- see how we can use bool both in custom syntax
-- and in "regular" Lean syntax

declare_syntax_cat foo
syntax "true" : foo
syntax "[foo|" foo "]" : term
macro_rules
| `([foo| true]) => `("true")

def succeeds : String := [foo| true]
def fails : Bool := true -- < ERROR: "expected term"

I'd like fails to not fail. That is, I'd like the context to disambiguate if I'm taking about truethat lives in the syntax category foo or in the Lean builtin category term.

[Siddharth Bhat]

A quick grep led me to two potential ways of doing this:

Lean/Parser/Command.lean
115:def optionValue := nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit

Lean/Parser/Term.lean
149:def trueVal  := leading_parser nonReservedSymbol "true"

but I'm unsure how to use nonReservedSymbol to achieve what I want.

[Jannis Limperg]

syntax &"true" : foo should be what you need. What happens here is that your syntax decl makes true into a keyword, so it doesn't get parsed as the identifier Bool.true any more. You might also need declare_syntax_cat foo (leading_ident_behavior := symbol).

[Leonardo de Moura]

@Siddharth Bhat We currently have a single token table in Lean. It is on our TODO list to have a separate table per syntax category, and rules for propagating reserved symbols between them. In the meantime, you can use the following workaround.

declare_syntax_cat foo
syntax ident : foo
syntax "[foo|" foo "]" : term

macro_rules
| `([foo| true]) => `("true")
| `([foo| false]) => `("false")

#check [foo| true]   -- "true"
#check [foo| false]  -- "false"
#check [foo| bla] -- error

[Siddharth Bhat]

Thank you for the perspective (that it's a TODO item). The idea of claiming to parse all identifiers and then selectively only parsing true and false, choosing to throw an error on the others is nice :)