parsing and collecting arguments as string

Stream: metaprogramming / tactics

[Xavier Martinet]

Hi,

I would like to parse a string that denotes an interactive tactic, and collect its arguments as a string

for instance, if the input is "try { norm_num }", I would like to be able to extract "norm_num"

I tried using <|>, but it did not work.

I do not understand what is wrong with that code :

meta def myparser := (do ident ← lean.parser.ident, guardb (ident = `aa), lean.parser.ident) <|> pure `zz
#eval lean.parser.run_with_input myparser "aa bb" >>= tactic.trace
-- bb
#eval lean.parser.run_with_input myparser "cc bb" >>= tactic.trace
-- failed