space separated sepBy?

Stream: lean4

[Siddharth Bhat]

How does one use "whitespace" separators for sepBy, such as spaces and newlines?

The code below works with the (commented) ; based separators, and does not with the (uncomment) space ( ) based separator. In particular, the declaration $kvs * is problematic. Is there some way to name the variable with the space?

declare_syntax_cat dict
-- syntax "<[" sepBy(str, ";") "]>" : dict
syntax "<[" sepBy(str, " ") "]>" : dict

set_option trace.Elab.definition true in
syntax "dict% " dict : term

macro_rules
  -- | `(dict% <[ $kvs;* ]> ) => do
  | `(dict% <[ $kvs * ]> ) => do
     let initList <- `([])
     kvs.getElems.foldlM (init := initList) fun xs kv => `($kv :: $xs )

def dict0 : List (String) := dict% <[  ]>
#print dict0

def dict1 : List String := dict% <[ "a" ; "b" ; "c" ]>
#print dict1

Errors:

crash.lean:4:0: error: invalid parser '«dict<[_]>»', invalid empty symbol
crash.lean:10:12: error: expected dict
crash.lean:14:35: error: expected dict
crash.lean:15:7: error: unknown constant 'dict0'
crash.lean:17:33: error: expected dict
crash.lean:18:7: error: unknown constant 'dict1'

[Mac]

You can just usestr* or (if you wish to demand whitespace) (ws str ws)*

[Mac]

For example:

declare_syntax_cat dict
syntax "<[" (ws str ws)* "]>" : dict

set_option trace.Elab.definition true in
syntax "dict% " dict : term

macro_rules
  | `(dict% <[ $[ $kvs ]* ]> ) => do
     let initList <- `([])
     kvs.foldlM (init := initList) fun xs kv => `($kv :: $xs )

def dict0 : List (String) := dict% <[  ]>
#print dict0

def dict1 : List String := dict% <[ "a" "b" "c" ]>
#print dict1