Zulip Chat Archive
Stream: metaprogramming / tactics
Topic: parsing a list of expressions
Chris Hughes (Jan 02 2021 at 17:51):
How do I feed a list of expressions into a tactic. In a similar way to how simp takes a list of expressions, but without any of the extra info that simp takes?
Chris Hughes (Jan 02 2021 at 17:57):
Is it parse (list_of texpr)?
Rob Lewis (Jan 02 2021 at 18:04):
Or docs#interactive.types.pexpr_list
Last updated: May 02 2025 at 03:31 UTC