Joseph Corneli (May 21 2019 at 13:12):
tactic.target >>= tactic.trace tells me the current main goal, but I would like to see all of the goals.
tactic.get_goals >>= tactic.trace has meta-variables in it. Is there a printer option that fills them in? I've forgotten.
Mario Carneiro (May 21 2019 at 13:15):
mmap infer_type get_goals >>= trace
Last updated: May 15 2021 at 23:13 UTC