Zulip Chat Archive
Stream: new members
Topic: optional arguments for tactics
Kevin Lacker (Dec 01 2020 at 17:23):
I'm confused on how to make optional arguments for tactics to work. Right now I have two different tactics, one of them takes an extra argument, and I want to make them just one tactic with that extra argument being optional:
meta def rewrite_search (try_harder : parse $ optional (tk "!"))
(cfg : config . pick_default) : tactic string :=
rewrite_search_target cfg []
meta def rewrite_search_with (try_harder : parse $ optional (tk "!")) (rs : parse rw_rules)
(cfg : config . pick_default) : tactic string :=
rewrite_search_target cfg rs.rules
From the docs I thought I should just be able to add a (rs : parse (optional rw_rules)) to the arguments for rewrite_search, but that causes my existing code to mis-parse.
Kevin Lacker (Dec 01 2020 at 17:38):
Last updated: Dec 20 2023 at 11:08 UTC